Documentation

Mathlib.Tactic.NormNum.Inv

norm_num plugins for Rat.cast and ⁻¹. #

def Mathlib.Meta.NormNum.inferCharZeroOfRing {u : Lean.Level} {α : Q(Type u)} (_i : Q(Ring «$α») := by with_reducible assumption) :
Lean.MetaM Q(CharZero «$α»)

Helper function to synthesize a typed CharZero α expression given Ring α.

Equations
    Instances For
      def Mathlib.Meta.NormNum.inferCharZeroOfRing? {u : Lean.Level} {α : Q(Type u)} (_i : Q(Ring «$α») := by with_reducible assumption) :

      Helper function to synthesize a typed CharZero α expression given Ring α, if it exists.

      Equations
        Instances For
          def Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne {u : Lean.Level} {α : Q(Type u)} (_i : Q(AddMonoidWithOne «$α») := by with_reducible assumption) :
          Lean.MetaM Q(CharZero «$α»)

          Helper function to synthesize a typed CharZero α expression given AddMonoidWithOne α.

          Equations
            Instances For
              def Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne? {u : Lean.Level} {α : Q(Type u)} (_i : Q(AddMonoidWithOne «$α») := by with_reducible assumption) :

              Helper function to synthesize a typed CharZero α expression given AddMonoidWithOne α, if it exists.

              Equations
                Instances For
                  def Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing {u : Lean.Level} {α : Q(Type u)} (_i : Q(DivisionRing «$α») := by with_reducible assumption) :
                  Lean.MetaM Q(CharZero «$α»)

                  Helper function to synthesize a typed CharZero α expression given DivisionRing α.

                  Equations
                    Instances For
                      def Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing? {u : Lean.Level} {α : Q(Type u)} (_i : Q(DivisionRing «$α») := by with_reducible assumption) :

                      Helper function to synthesize a typed CharZero α expression given DivisionRing α, if it exists.

                      Equations
                        Instances For
                          theorem Mathlib.Meta.NormNum.isRat_mkRat {a na n : } {b nb d : } :
                          IsInt a naIsNat b nbIsRat (na / nb) n dIsRat (mkRat a b) n d

                          The norm_num extension which identifies expressions of the form mkRat a b, such that norm_num successfully recognises both a and b, and returns a / b.

                          Equations
                            Instances For
                              theorem Mathlib.Meta.NormNum.isNat_ratCast {R : Type u_1} [DivisionRing R] {q : } {n : } :
                              IsNat q nIsNat (↑q) n
                              theorem Mathlib.Meta.NormNum.isInt_ratCast {R : Type u_1} [DivisionRing R] {q : } {n : } :
                              IsInt q nIsInt (↑q) n
                              theorem Mathlib.Meta.NormNum.isRat_ratCast {R : Type u_1} [DivisionRing R] [CharZero R] {q : } {n : } {d : } :
                              IsRat q n dIsRat (↑q) n d

                              The norm_num extension which identifies an expression RatCast.ratCast q where norm_num recognizes q, returning the cast of q.

                              Equations
                                Instances For
                                  theorem Mathlib.Meta.NormNum.isRat_inv_pos {α : Type u_1} [DivisionRing α] [CharZero α] {a : α} {n d : } :
                                  theorem Mathlib.Meta.NormNum.isRat_inv_one {α : Type u_1} [DivisionRing α] {a : α} :
                                  IsNat a 1IsNat a⁻¹ 1
                                  theorem Mathlib.Meta.NormNum.isRat_inv_zero {α : Type u_1} [DivisionRing α] {a : α} :
                                  IsNat a 0IsNat a⁻¹ 0
                                  theorem Mathlib.Meta.NormNum.isRat_inv_neg {α : Type u_1} [DivisionRing α] [CharZero α] {a : α} {n d : } :

                                  The norm_num extension which identifies expressions of the form a⁻¹, such that norm_num successfully recognises a.

                                  Equations
                                    Instances For
                                      def Mathlib.Meta.NormNum.evalInv.core {u : Lean.Level} {α : Q(Type u)} (e a : Q(«$α»)) (ra : Result a) ( : Q(DivisionRing «$α»)) (i : Option Q(CharZero «$α»)) :

                                      Main part of evalInv.

                                      Equations
                                        Instances For