Documentation

Mathlib.Tactic.ArithMult

Multiplicativity #

We define the arith_mult tactic using aesop

source
def ArithmeticFunction.attrArith_mult :
Lean.ParserDescr

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

Equations
    Instances For
      source
      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
        Instances For
          source
          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
            Instances For