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
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
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.
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
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)
:
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
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
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)
:
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)
:
(In)equalities #
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
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)
:
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
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
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)
:
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)
:
def
Mathlib.Meta.NormNum.evalLE.core
{u : Lean.Level}
{α : Q(Type u)}
(lα : Q(LE «$α»))
{a : Q(«$α»)}
{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.
def
Mathlib.Meta.NormNum.evalLE.core.intArm
{u : Lean.Level}
{α : Q(Type u)}
(lα : Q(LE «$α»))
{a : Q(«$α»)}
{b : Q(«$α»)}
(ra : Mathlib.Meta.NormNum.Result a)
(rb : Mathlib.Meta.NormNum.Result b)
(e : Q(Prop))
:
Equations
- One or more equations did not get rendered due to their size.
def
Mathlib.Meta.NormNum.evalLE.core.ratArm
{u : Lean.Level}
{α : Q(Type u)}
(lα : Q(LE «$α»))
{a : Q(«$α»)}
{b : Q(«$α»)}
(ra : Mathlib.Meta.NormNum.Result a)
(rb : Mathlib.Meta.NormNum.Result b)
(e : Q(Prop))
:
Equations
- One or more equations did not get rendered due to their size.
def
Mathlib.Meta.NormNum.evalLT.core
{u : Lean.Level}
{α : Q(Type u)}
(lα : Q(LT «$α»))
{a : Q(«$α»)}
{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.
def
Mathlib.Meta.NormNum.evalLT.core.intArm
{u : Lean.Level}
{α : Q(Type u)}
(lα : Q(LT «$α»))
{a : Q(«$α»)}
{b : Q(«$α»)}
(ra : Mathlib.Meta.NormNum.Result a)
(rb : Mathlib.Meta.NormNum.Result b)
(e : Q(Prop))
:
Equations
- One or more equations did not get rendered due to their size.
def
Mathlib.Meta.NormNum.evalLT.core.ratArm
{u : Lean.Level}
{α : Q(Type u)}
(lα : Q(LT «$α»))
{a : Q(«$α»)}
{b : Q(«$α»)}
(ra : Mathlib.Meta.NormNum.Result a)
(rb : Mathlib.Meta.NormNum.Result b)
(e : Q(Prop))
:
Equations
- One or more equations did not get rendered due to their size.