Multiplicativity

We define the arith_mult tactic using aesop

def ArithmeticFunction.attrArith_mult : Lean.ParserDescr

The arith_mult attribute used to tag IsMultiplicative statements for the arith_mult tactic.

Equations

• ArithmeticFunction.attrArith_mult = Lean.ParserDescr.node `ArithmeticFunction.attrArith_mult 1024 (Lean.ParserDescr.nonReservedSymbol "arith_mult" false)

def ArithmeticFunction.arith_mult : Lean.ParserDescr

arith_mult solves goals of the form IsMultiplicative f for f : ArithmeticFunction R by applying lemmas tagged with the user attribute arith_mult.

Equations

• One or more equations did not get rendered due to their size.

def ArithmeticFunction.arith_mult? : Lean.ParserDescr

arith_mult solves goals of the form IsMultiplicative f for f : ArithmeticFunction R by applying lemmas tagged with the user attribute arith_mult, and prints out the generated proof term.

Equations

• One or more equations did not get rendered due to their size.