norm_num extensions for inequalities. #

Helper function to synthesize a typed OrderedSemiring α expression.

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

Helper function to synthesize a typed OrderedRing α expression.

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

Helper function to synthesize a typed LinearOrderedField α expression.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Mathlib.Meta.NormNum.isNat_le_true {α : Type u_1} [] {a : α} {b : α} {a' : } {b' : } :
a'.ble b' = truea b
theorem Mathlib.Meta.NormNum.isNat_lt_false {α : Type u_1} [] {a : α} {b : α} {a' : } {b' : } (ha : ) (hb : ) (h : b'.ble a' = true) :
¬a < b
theorem Mathlib.Meta.NormNum.isRat_le_true {α : Type u_1} {a : α} {b : α} {na : } {nb : } {da : } {db : } :
decide (na.mul () nb.mul ()) = truea b
theorem Mathlib.Meta.NormNum.isRat_lt_true {α : Type u_1} [] {a : α} {b : α} {na : } {nb : } {da : } {db : } :
decide (na * db < nb * da) = truea < b
theorem Mathlib.Meta.NormNum.isRat_le_false {α : Type u_1} [] {a : α} {b : α} {na : } {nb : } {da : } {db : } (ha : ) (hb : ) (h : decide (nb * da < na * db) = true) :
¬a b
theorem Mathlib.Meta.NormNum.isRat_lt_false {α : Type u_1} {a : α} {b : α} {na : } {nb : } {da : } {db : } (ha : ) (hb : ) (h : decide (nb * da na * db) = true) :
¬a < b

(In)equalities #

theorem Mathlib.Meta.NormNum.isNat_lt_true {α : Type u_1} [] [] {a : α} {b : α} {a' : } {b' : } :
b'.ble a' = falsea < b
theorem Mathlib.Meta.NormNum.isNat_le_false {α : Type u_1} [] [] {a : α} {b : α} {a' : } {b' : } (ha : ) (hb : ) (h : a'.ble b' = false) :
¬a b
theorem Mathlib.Meta.NormNum.isInt_le_true {α : Type u_1} [] {a : α} {b : α} {a' : } {b' : } :
decide (a' b') = truea b
theorem Mathlib.Meta.NormNum.isInt_lt_true {α : Type u_1} [] [] {a : α} {b : α} {a' : } {b' : } :
decide (a' < b') = truea < b
theorem Mathlib.Meta.NormNum.isInt_le_false {α : Type u_1} [] [] {a : α} {b : α} {a' : } {b' : } (ha : ) (hb : ) (h : decide (b' < a') = true) :
¬a b
theorem Mathlib.Meta.NormNum.isInt_lt_false {α : Type u_1} [] {a : α} {b : α} {a' : } {b' : } (ha : ) (hb : ) (h : decide (b' a') = true) :
¬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.evalLE.intArm {v : Lean.Level} {β : Q(Type v)} (e : Q(«$β»)) (f : Lean.Expr) (u : Lean.Level) (α : let u := u; Q(Type u)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : ) (rb : ) : Equations • One or more equations did not get rendered due to their size. Instances For def Mathlib.Meta.NormNum.evalLE.ratArm {v : Lean.Level} {β : Q(Type v)} (e : Q(«$β»)) (f : Lean.Expr) (u : Lean.Level) (α : let u := u; Q(Type u)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : ) (rb : ) :
Equations
• One or more equations did not get rendered due to their size.
Instances For

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.evalLT.intArm {v : Lean.Level} {β : Q(Type v)} (e : Q(«$β»)) (f : Lean.Expr) (u : Lean.Level) (α : let u := u; Q(Type u)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : ) (rb : ) : Equations • One or more equations did not get rendered due to their size. Instances For def Mathlib.Meta.NormNum.evalLT.ratArm {v : Lean.Level} {β : Q(Type v)} (e : Q(«$β»)) (f : Lean.Expr) (u : Lean.Level) (α : let u := u; Q(Type u)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : ) (rb : ) :
Equations
• One or more equations did not get rendered due to their size.
Instances For