Documentation

Mathlib.Tactic.ArithMult

Multiplicativity #

We define the arith_mult tactic using aesop

source
🔸 coverage
def ArithmeticFunction.attrArith_mult :
Lean.ParserDescr

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

Instances For
    source
    🔸 coverage
    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.

    Instances For
      source
      🔸 coverage
      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.

      Instances For