norm_num extension for equalities

theorem Mathlib.Meta.NormNum.isNat_eq_false {α : Type u_1} [AddMonoidWithOne α] [CharZero α] {a b : α} {a' b' : ℕ} : Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → a'.beq b' = false → ¬a = b

theorem Mathlib.Meta.NormNum.isInt_eq_false {α : Type u_1} [Ring α] [CharZero α] {a b : α} {a' b' : ℤ} : Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → decide (a' = b') = false → ¬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 da → Mathlib.Meta.NormNum.IsRat b nb db → decide (na.mul (Int.ofNat db) = nb.mul (Int.ofNat da)) = false → ¬a = b

def Mathlib.Meta.NormNum.evalEq : Mathlib.Meta.NormNum.NormNumExt

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.

def Mathlib.Meta.NormNum.evalEq.intArm {v : Lean.Level} {β : Q(Type v)} (e : Q(«$β»)) (u : Lean.Level) (α : let u := u; Q(Type u)) (a b : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) (rα : Q(Ring «$α»)) : Lean.MetaM (Mathlib.Meta.NormNum.Result e)

Equations

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

def Mathlib.Meta.NormNum.evalEq.ratArm {v : Lean.Level} {β : Q(Type v)} (e : Q(«$β»)) (u : Lean.Level) (α : let u := u; Q(Type u)) (a b : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) (dα : Q(DivisionRing «$α»)) : Lean.MetaM (Mathlib.Meta.NormNum.Result e)

Equations

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