# `norm_num` extensions for inequalities. #

source
def Mathlib.Meta.NormNum.inferOrderedSemiring {u : Lean.Level} (α : Q(Type u)) :
Lean.MetaM ((x : Q(Semiring «$α»)) × (x_1 : Q(PartialOrder «$α»)) × Q(IsOrderedRing «$α»))

Helper function to synthesize typed `Semiring α` `PartialOrder α` `IsOrderedSemiring α` expressions.

Equations

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

Instances For

source
def Mathlib.Meta.NormNum.inferOrderedRing {u : Lean.Level} (α : Q(Type u)) :
Lean.MetaM ((x : Q(Ring «$α»)) × (x_1 : Q(PartialOrder «$α»)) × Q(IsOrderedRing «$α»))

Helper function to synthesize typed `Ring α` `PartialOrder α` `IsOrderedSemiring α` expressions.

Equations

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

Instances For

source
def Mathlib.Meta.NormNum.inferLinearOrderedSemifield {u : Lean.Level} (α : Q(Type u)) :
Lean.MetaM ((x : Q(Semifield «$α»)) × (x_1 : Q(LinearOrder «$α»)) × Q(IsStrictOrderedRing «$α»))

Helper function to synthesize typed `Semifield α` `LinearOrder α` `IsStrictOrderedRing α` expressions.

Equations

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

Instances For

source
def Mathlib.Meta.NormNum.inferLinearOrderedField {u : Lean.Level} (α : Q(Type u)) :
Lean.MetaM ((x : Q(Field «$α»)) × (x_1 : Q(LinearOrder «$α»)) × Q(IsStrictOrderedRing «$α»))

Helper function to synthesize typed `Field α` `LinearOrder α` `IsStrictOrderedRing α` expressions.

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} [Semiring α] [PartialOrder α] [IsOrderedRing α] {a b : α} {a' b' : ℕ} :
IsNat a a' → IsNat b b' → a'.ble b' = true → a ≤ b
source
theorem Mathlib.Meta.NormNum.isNat_lt_false {α : Type u_1} [Semiring α] [PartialOrder α] [IsOrderedRing α] {a b : α} {a' b' : ℕ} (ha : IsNat a a') (hb : IsNat b b') (h : b'.ble a' = true) :
¬a < b
source
theorem Mathlib.Meta.NormNum.isNNRat_le_true {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} {na nb da db : ℕ} :
IsNNRat a na da → IsNNRat b nb db → decide (na.mul db ≤ nb.mul da) = true → a ≤ b
source
theorem Mathlib.Meta.NormNum.isNNRat_lt_true {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [Nontrivial α] {a b : α} {na nb da db : ℕ} :
IsNNRat a na da → IsNNRat b nb db → decide (na * db < nb * da) = true → a < b
source
theorem Mathlib.Meta.NormNum.isNNRat_le_false {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [Nontrivial α] {a b : α} {na nb da db : ℕ} (ha : IsNNRat a na da) (hb : IsNNRat b nb db) (h : decide (nb * da < na * db) = true) :
¬a ≤ b
source
theorem Mathlib.Meta.NormNum.isNNRat_lt_false {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} {na nb da db : ℕ} (ha : IsNNRat a na da) (hb : IsNNRat b nb db) (h : decide (nb * da ≤ na * db) = true) :
¬a < b
source
theorem Mathlib.Meta.NormNum.isRat_le_true {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} {na nb : ℤ} {da db : ℕ} :
IsRat a na da → 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} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [Nontrivial α] {a b : α} {na nb : ℤ} {da db : ℕ} :
IsRat a na da → IsRat b nb db → decide (na * ↑db < nb * ↑da) = true → a < b
source
theorem Mathlib.Meta.NormNum.isRat_le_false {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [Nontrivial α] {a b : α} {na nb : ℤ} {da db : ℕ} (ha : IsRat a na da) (hb : IsRat b nb db) (h : decide (nb * ↑da < na * ↑db) = true) :
¬a ≤ b
source
theorem Mathlib.Meta.NormNum.isRat_lt_false {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} {na nb : ℤ} {da db : ℕ} (ha : IsRat a na da) (hb : 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} [Semiring α] [PartialOrder α] [IsOrderedRing α] [CharZero α] {a b : α} {a' b' : ℕ} :
IsNat a a' → IsNat b b' → b'.ble a' = false → a < b
source
theorem Mathlib.Meta.NormNum.isNat_le_false {α : Type u_1} [Semiring α] [PartialOrder α] [IsOrderedRing α] [CharZero α] {a b : α} {a' b' : ℕ} (ha : IsNat a a') (hb : IsNat b b') (h : a'.ble b' = false) :
¬a ≤ b
source
theorem Mathlib.Meta.NormNum.isInt_le_true {α : Type u_1} [Ring α] [PartialOrder α] [IsOrderedRing α] {a b : α} {a' b' : ℤ} :
IsInt a a' → IsInt b b' → decide (a' ≤ b') = true → a ≤ b
source
theorem Mathlib.Meta.NormNum.isInt_lt_true {α : Type u_1} [Ring α] [PartialOrder α] [IsOrderedRing α] [Nontrivial α] {a b : α} {a' b' : ℤ} :
IsInt a a' → IsInt b b' → decide (a' < b') = true → a < b
source
theorem Mathlib.Meta.NormNum.isInt_le_false {α : Type u_1} [Ring α] [PartialOrder α] [IsOrderedRing α] [Nontrivial α] {a b : α} {a' b' : ℤ} (ha : IsInt a a') (hb : IsInt b b') (h : decide (b' < a') = true) :
¬a ≤ b
source
theorem Mathlib.Meta.NormNum.isInt_lt_false {α : Type u_1} [Ring α] [PartialOrder α] [IsOrderedRing α] {a b : α} {a' b' : ℤ} (ha : IsInt a a') (hb : IsInt b b') (h : decide (b' ≤ a') = true) :
¬a < b
source
def Mathlib.Meta.NormNum.evalLE :
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 : Result a) (rb : Result b) :
Lean.MetaM (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.

Equations

- One or more equations did not get rendered due to their size.
- Mathlib.Meta.NormNum.evalLE.core lα (Mathlib.Meta.NormNum.Result'.isBool val proof) rb = failure
- Mathlib.Meta.NormNum.evalLE.core lα ra (Mathlib.Meta.NormNum.Result'.isBool val proof) = failure
- Mathlib.Meta.NormNum.evalLE.core lα (Mathlib.Meta.NormNum.Result'.isNegNat inst lit proof) rb = Mathlib.Meta.NormNum.evalLE.core.intArm lα (Mathlib.Meta.NormNum.Result'.isNegNat inst lit proof) rb
- Mathlib.Meta.NormNum.evalLE.core lα ra (Mathlib.Meta.NormNum.Result'.isNegNat inst lit proof) = Mathlib.Meta.NormNum.evalLE.core.intArm lα ra (Mathlib.Meta.NormNum.Result'.isNegNat inst lit proof)

Instances For

source
def Mathlib.Meta.NormNum.evalLE.core.intArm {u : Lean.Level} {α : Q(Type u)} (lα : Q(LE «$α»)) {a b : Q(«$α»)} (ra : Result a) (rb : Result b) :
have e := q(«$a» ≤ «$b»); Lean.MetaM (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 : Result a) (rb : Result b) :
have e := q(«$a» ≤ «$b»); Lean.MetaM (Result e)
Equations

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

Instances For

source
def Mathlib.Meta.NormNum.evalLT :
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 : Result a) (rb : Result b) :
Lean.MetaM (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.

Equations

- One or more equations did not get rendered due to their size.
- Mathlib.Meta.NormNum.evalLT.core lα (Mathlib.Meta.NormNum.Result'.isBool val proof) rb = failure
- Mathlib.Meta.NormNum.evalLT.core lα ra (Mathlib.Meta.NormNum.Result'.isBool val proof) = failure
- Mathlib.Meta.NormNum.evalLT.core lα (Mathlib.Meta.NormNum.Result'.isNegNat inst lit proof) rb = Mathlib.Meta.NormNum.evalLT.core.intArm lα (Mathlib.Meta.NormNum.Result'.isNegNat inst lit proof) rb
- Mathlib.Meta.NormNum.evalLT.core lα ra (Mathlib.Meta.NormNum.Result'.isNegNat inst lit proof) = Mathlib.Meta.NormNum.evalLT.core.intArm lα ra (Mathlib.Meta.NormNum.Result'.isNegNat inst lit proof)

Instances For

source
def Mathlib.Meta.NormNum.evalLT.core.intArm {u : Lean.Level} {α : Q(Type u)} (lα : Q(LT «$α»)) {a b : Q(«$α»)} (ra : Result a) (rb : Result b) :
have e := q(«$a» < «$b»); Lean.MetaM (Result e)
Equations

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

Instances For

source
def Mathlib.Meta.NormNum.evalLT.core.nnratArm {u : Lean.Level} {α : Q(Type u)} (lα : Q(LT «$α»)) {a b : Q(«$α»)} (ra : Result a) (rb : Result b) :
have e := q(«$a» < «$b»); Lean.MetaM (Result e)
Equations

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

Instances For

source
def Mathlib.Meta.NormNum.evalLT.core.ratArm {u : Lean.Level} {α : Q(Type u)} (lα : Q(LT «$α»)) {a b : Q(«$α»)} (ra : Result a) (rb : Result b) :
have e := q(«$a» < «$b»); Lean.MetaM (Result e)
Equations

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

Instances For