Documentation

Mathlib.Tactic.NormNum.Eq

norm_num extension for equalities #

theorem Mathlib.Meta.NormNum.isNat_eq_false {α : Type u_1} [AddMonoidWithOne α] [CharZero α] {a : α} {b : α} {a' : } {b' : } :
theorem Mathlib.Meta.NormNum.isInt_eq_false {α : Type u_1} [Ring α] [CharZero α] {a : α} {b : α} {a' : } {b' : } :
theorem Mathlib.Meta.NormNum.Rat.invOf_denom_swap {α : Type u_1} [Ring α] (n₁ : ) (n₂ : ) (a₁ : α) (a₂ : α) [Invertible a₁] [Invertible a₂] :
n₁ * a₁ = n₂ * a₂ n₁ * a₂ = n₂ * a₁
theorem Mathlib.Meta.NormNum.isRat_eq_false {α : Type u_1} [Ring α] [CharZero α] {a : α} {b : α} {na : } {nb : } {da : } {db : } :
Mathlib.Meta.NormNum.IsRat a na daMathlib.Meta.NormNum.IsRat b nb dbdecide (na.mul (Int.ofNat db) = nb.mul (Int.ofNat da)) = false¬a = b

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def Mathlib.Meta.NormNum.evalEq.intArm {v : Lean.Level} {β : Q(Type v)} (e : Q(«$β»)) (u : Lean.Level) (α : let u := u; Q(Type u)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) (rα : Q(Ring «$α»)) :
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def Mathlib.Meta.NormNum.evalEq.ratArm {v : Lean.Level} {β : Q(Type v)} (e : Q(«$β»)) (u : Lean.Level) (α : let u := u; Q(Type u)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) (dα : Q(DivisionRing «$α»)) :
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For