`norm_num` extensions for inequalities. #

source

def Mathlib.Meta.NormNum.inferOrderedSemiring {u : Lean.Level} (α : Q(Type u)) :

Lean.MetaM Q(OrderedSemiring «$α»)

Helper function to synthesize a typed OrderedSemiring α expression.

Equations

Mathlib.Meta.NormNum.inferOrderedSemiring α = do let __do_lift ← Qq.synthInstanceQ q(OrderedSemiring «$α») <|> Lean.throwError (Lean.toMessageData "not an ordered semiring") pure __do_lift

Instances For

source

def Mathlib.Meta.NormNum.inferOrderedRing {u : Lean.Level} (α : Q(Type u)) :

Lean.MetaM Q(OrderedRing «$α»)

Helper function to synthesize a typed OrderedRing α expression.

Equations

Mathlib.Meta.NormNum.inferOrderedRing α = do let __do_lift ← Qq.synthInstanceQ q(OrderedRing «$α») <|> Lean.throwError (Lean.toMessageData "not an ordered ring") pure __do_lift

Instances For

source

def Mathlib.Meta.NormNum.inferLinearOrderedField {u : Lean.Level} (α : Q(Type u)) :

Lean.MetaM Q(LinearOrderedField «$α»)

Helper function to synthesize a typed LinearOrderedField α expression.

Equations

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

Instances For

source

theorem Mathlib.Meta.NormNum.isNat_le_true {α : Type u_1} [OrderedSemiring α] {a b : α} {a' b' : ℕ} :

Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → a'.ble b' = true → a ≤ b

source

theorem Mathlib.Meta.NormNum.isNat_lt_false {α : Type u_1} [OrderedSemiring α] {a b : α} {a' b' : ℕ} (ha : Mathlib.Meta.NormNum.IsNat a a') (hb : Mathlib.Meta.NormNum.IsNat b b') (h : b'.ble a' = true) :

¬a < b

source

theorem Mathlib.Meta.NormNum.isRat_le_true {α : Type u_1} [LinearOrderedRing α] {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)) = true → a ≤ b

source

theorem Mathlib.Meta.NormNum.isRat_lt_true {α : Type u_1} [LinearOrderedRing α] [Nontrivial α] {a b : α} {na nb : ℤ} {da db : ℕ} :

Mathlib.Meta.NormNum.IsRat a na da → Mathlib.Meta.NormNum.IsRat b nb db → decide (na * ↑db < nb * ↑da) = true → a < b

source

theorem Mathlib.Meta.NormNum.isRat_le_false {α : Type u_1} [LinearOrderedRing α] [Nontrivial α] {a b : α} {na nb : ℤ} {da db : ℕ} (ha : Mathlib.Meta.NormNum.IsRat a na da) (hb : Mathlib.Meta.NormNum.IsRat b nb db) (h : decide (nb * ↑da < na * ↑db) = true) :

¬a ≤ b

source

theorem Mathlib.Meta.NormNum.isRat_lt_false {α : Type u_1} [LinearOrderedRing α] {a b : α} {na nb : ℤ} {da db : ℕ} (ha : Mathlib.Meta.NormNum.IsRat a na da) (hb : Mathlib.Meta.NormNum.IsRat b nb db) (h : decide (nb * ↑da ≤ na * ↑db) = true) :

¬a < b

(In)equalities #

source

theorem Mathlib.Meta.NormNum.isNat_lt_true {α : Type u_1} [OrderedSemiring α] [CharZero α] {a b : α} {a' b' : ℕ} :

Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → b'.ble a' = false → a < b

source

theorem Mathlib.Meta.NormNum.isNat_le_false {α : Type u_1} [OrderedSemiring α] [CharZero α] {a b : α} {a' b' : ℕ} (ha : Mathlib.Meta.NormNum.IsNat a a') (hb : Mathlib.Meta.NormNum.IsNat b b') (h : a'.ble b' = false) :

¬a ≤ b

source

theorem Mathlib.Meta.NormNum.isInt_le_true {α : Type u_1} [OrderedRing α] {a b : α} {a' b' : ℤ} :

Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → decide (a' ≤ b') = true → a ≤ b

source

theorem Mathlib.Meta.NormNum.isInt_lt_true {α : Type u_1} [OrderedRing α] [Nontrivial α] {a b : α} {a' b' : ℤ} :

Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → decide (a' < b') = true → a < b

source

theorem Mathlib.Meta.NormNum.isInt_le_false {α : Type u_1} [OrderedRing α] [Nontrivial α] {a b : α} {a' b' : ℤ} (ha : Mathlib.Meta.NormNum.IsInt a a') (hb : Mathlib.Meta.NormNum.IsInt b b') (h : decide (b' < a') = true) :

¬a ≤ b

source

theorem Mathlib.Meta.NormNum.isInt_lt_false {α : Type u_1} [OrderedRing α] {a b : α} {a' b' : ℤ} (ha : Mathlib.Meta.NormNum.IsInt a a') (hb : Mathlib.Meta.NormNum.IsInt b b') (h : decide (b' ≤ a') = true) :

¬a < b

source

def Mathlib.Meta.NormNum.evalLE :

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.

Instances For

source

def Mathlib.Meta.NormNum.evalLE.core {u : Lean.Level} {α : Q(Type u)} (lα : Q(LE «$α»)) {a b : Q(«$α»)} (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) :

Lean.MetaM (Mathlib.Meta.NormNum.Result q(«$a» ≤ «$b»))

Identify (as true or false) expressions of the form a ≤ b, where a and b are numeric expressions whose evaluations to NormNum.Result have already been computed.

Instances For

source

def Mathlib.Meta.NormNum.evalLE.core.intArm {u : Lean.Level} {α : Q(Type u)} (lα : Q(LE «$α»)) {a b : Q(«$α»)} (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) (e : Q(Prop)) :

Lean.MetaM (Mathlib.Meta.NormNum.Result e)

Equations

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

Instances For

source

def Mathlib.Meta.NormNum.evalLE.core.ratArm {u : Lean.Level} {α : Q(Type u)} (lα : Q(LE «$α»)) {a b : Q(«$α»)} (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) (e : Q(Prop)) :

Lean.MetaM (Mathlib.Meta.NormNum.Result e)

Equations

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

Instances For

source

def Mathlib.Meta.NormNum.evalLT :

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.

Instances For

source

def Mathlib.Meta.NormNum.evalLT.core {u : Lean.Level} {α : Q(Type u)} (lα : Q(LT «$α»)) {a b : Q(«$α»)} (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) :

Lean.MetaM (Mathlib.Meta.NormNum.Result q(«$a» < «$b»))

Identify (as true or false) expressions of the form a < b, where a and b are numeric expressions whose evaluations to NormNum.Result have already been computed.

Instances For

source