`norm_num` basic plugins #

This file adds norm_num plugins for +, * and ^ along with other basic operations.

The norm_num extension which identifies the expression Zero.zero, returning 0.

Equations

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

source

ink

theorem Mathlib.Meta.NormNum.isNat_one (α : Type u_1) [inst : AddMonoidWithOne α] :

Mathlib.Meta.NormNum.IsNat One.one 1

source

ink

def Mathlib.Meta.NormNum.evalOne :

Mathlib.Meta.NormNum.NormNumExt

The norm_num extension which identifies the expression One.one, returning 1.

Equations

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

source

ink

theorem Mathlib.Meta.NormNum.isNat_ofNat (α : Type u_1) [inst : AddMonoidWithOne α] {a : α} {n : ℕ} (h : ↑n = a) :

Mathlib.Meta.NormNum.IsNat a n

source

ink

def Mathlib.Meta.NormNum.evalOfNat :

Mathlib.Meta.NormNum.NormNumExt

The norm_num extension which identifies an expression OfNat.ofNat n, returning n.

Equations

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

source

ink

theorem Mathlib.Meta.NormNum.isNat_cast {R : Type u_1} [inst : AddMonoidWithOne R] (n : ℕ) (m : ℕ) :

Mathlib.Meta.NormNum.IsNat n m → Mathlib.Meta.NormNum.IsNat (↑n) m

source

ink

def Mathlib.Meta.NormNum.evalNatCast :

Mathlib.Meta.NormNum.NormNumExt

The norm_num extension which identifies an expression Nat.cast n, returning n.

Equations

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

source

ink

theorem Mathlib.Meta.NormNum.isNat_int_cast {R : Type u_1} [inst : Ring R] (n : ℤ) (m : ℕ) :

Mathlib.Meta.NormNum.IsNat n m → Mathlib.Meta.NormNum.IsNat (↑n) m

source

ink

theorem Mathlib.Meta.NormNum.isInt_cast {R : Type u_1} [inst : Ring R] (n : ℤ) (m : ℤ) :

Mathlib.Meta.NormNum.IsInt n m → Mathlib.Meta.NormNum.IsInt (↑n) m

source

ink

def Mathlib.Meta.NormNum.evalIntCast :

Mathlib.Meta.NormNum.NormNumExt

The norm_num extension which identifies an expression Int.cast n, returning n.

Equations

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

source

ink

theorem Mathlib.Meta.NormNum.isNat_add {α : Type u_1} [inst : AddMonoidWithOne α] {a : α} {b : α} {a' : ℕ} {b' : ℕ} {c : ℕ} :

Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → Nat.add a' b' = c → Mathlib.Meta.NormNum.IsNat (a + b) c

source

ink

theorem Mathlib.Meta.NormNum.isInt_add {α : Type u_1} [inst : Ring α] {a : α} {b : α} {a' : ℤ} {b' : ℤ} {c : ℤ} :

Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → Int.add a' b' = c → Mathlib.Meta.NormNum.IsInt (a + b) c

source

ink

def Mathlib.Meta.NormNum.invertibleOfMul {α : Type u_1} [inst : Semiring α] (k : ℕ) (b : α) (a : α) [inst : Invertible a] :

a = ↑k * b → Invertible b

If b divides a and a is invertible, then b is invertible.

Equations

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

source

ink

def Mathlib.Meta.NormNum.invertibleOfMul' {α : Type u_1} [inst : Semiring α] {a : ℕ} {k : ℕ} {b : ℕ} [inst : Invertible ↑a] (h : a = k * b) :

Invertible ↑b

If b divides a and a is invertible, then b is invertible.

Equations

Mathlib.Meta.NormNum.invertibleOfMul' h = Mathlib.Meta.NormNum.invertibleOfMul k ↑b ↑a (_ : ↑a = ↑k * ↑b)

source

ink

theorem Mathlib.Meta.NormNum.isRat_add {α : Type u_1} [inst : Ring α] {a : α} {b : α} {na : ℤ} {nb : ℤ} {nc : ℤ} {da : ℕ} {db : ℕ} {dc : ℕ} {k : ℕ} :

Mathlib.Meta.NormNum.IsRat a na da → Mathlib.Meta.NormNum.IsRat b nb db → Int.add (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc → Nat.mul da db = Nat.mul k dc → Mathlib.Meta.NormNum.IsRat (a + b) nc dc

source

ink

instance Mathlib.Meta.NormNum.instMonadLiftOptionMetaM :

MonadLift Option Lean.MetaM

Equations

Mathlib.Meta.NormNum.instMonadLiftOptionMetaM = { monadLift := fun {α} x => match x with | none => failure | some e => pure e }

source

ink

def Mathlib.Meta.NormNum.evalAdd :

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.

source

ink

def Mathlib.Meta.NormNum.evalAdd.core {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (e : Qq.QQ α) (a : Qq.QQ α) (b : Qq.QQ α) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) :

Option (Mathlib.Meta.NormNum.Result e)

Main part of evalAdd.

Equations

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

source

ink

theorem Mathlib.Meta.NormNum.isInt_neg {α : Type u_1} [inst : Ring α] {a : α} {a' : ℤ} {b : ℤ} :

Mathlib.Meta.NormNum.IsInt a a' → Int.neg a' = b → Mathlib.Meta.NormNum.IsInt (-a) b

source

ink

theorem Mathlib.Meta.NormNum.isRat_neg {α : Type u_1} [inst : Ring α] {a : α} {n : ℤ} {n' : ℤ} {d : ℕ} :

Mathlib.Meta.NormNum.IsRat a n d → Int.neg n = n' → Mathlib.Meta.NormNum.IsRat (-a) n' d

source

ink

def Mathlib.Meta.NormNum.evalNeg :

Mathlib.Meta.NormNum.NormNumExt

The norm_num extension which identifies expressions of the form -a, such that norm_num successfully recognises a.

Equations

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

source

ink

def Mathlib.Meta.NormNum.evalNeg.core {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (e : Qq.QQ α) (a : Qq.QQ α) (ra : Mathlib.Meta.NormNum.Result a) (rα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `Ring [u]) α)) :

Option (Mathlib.Meta.NormNum.Result e)

Main part of evalNeg.

Equations

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

source

ink

theorem Mathlib.Meta.NormNum.isInt_sub {α : Type u_1} [inst : Ring α] {a : α} {b : α} {a' : ℤ} {b' : ℤ} {c : ℤ} :

Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → Int.sub a' b' = c → Mathlib.Meta.NormNum.IsInt (a - b) c

source

ink

theorem Mathlib.Meta.NormNum.isRat_sub {α : Type u_1} [inst : Ring α] {a : α} {b : α} {na : ℤ} {nb : ℤ} {nc : ℤ} {da : ℕ} {db : ℕ} {dc : ℕ} {k : ℕ} (ra : Mathlib.Meta.NormNum.IsRat a na da) (rb : Mathlib.Meta.NormNum.IsRat b nb db) (h₁ : Int.sub (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc) (h₂ : Nat.mul da db = Nat.mul k dc) :

Mathlib.Meta.NormNum.IsRat (a - b) nc dc

source

ink

def Mathlib.Meta.NormNum.evalSub :

Mathlib.Meta.NormNum.NormNumExt

The norm_num extension which identifies expressions of the form a - b in a ring, such that norm_num successfully recognises both a and b.

Equations

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

source

ink

def Mathlib.Meta.NormNum.evalSub.core {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (e : Qq.QQ α) (a : Qq.QQ α) (b : Qq.QQ α) (rα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `Ring [u]) α)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) :

Option (Mathlib.Meta.NormNum.Result e)

Main part of evalAdd.

Equations

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

source

ink

theorem Mathlib.Meta.NormNum.isNat_mul {α : Type u_1} [inst : Semiring α] {a : α} {b : α} {a' : ℕ} {b' : ℕ} {c : ℕ} :

Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → Nat.mul a' b' = c → Mathlib.Meta.NormNum.IsNat (a * b) c

source

ink

theorem Mathlib.Meta.NormNum.isInt_mul {α : Type u_1} [inst : Ring α] {a : α} {b : α} {a' : ℤ} {b' : ℤ} {c : ℤ} :

Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → Int.mul a' b' = c → Mathlib.Meta.NormNum.IsInt (a * b) c

source

ink

theorem Mathlib.Meta.NormNum.isRat_mul {α : Type u_1} [inst : Ring α] {a : α} {b : α} {na : ℤ} {nb : ℤ} {nc : ℤ} {da : ℕ} {db : ℕ} {dc : ℕ} {k : ℕ} :

Mathlib.Meta.NormNum.IsRat a na da → Mathlib.Meta.NormNum.IsRat b nb db → Int.mul na nb = Int.mul (↑k) nc → Nat.mul da db = Nat.mul k dc → Mathlib.Meta.NormNum.IsRat (a * b) nc dc

source

ink

def Mathlib.Meta.NormNum.evalMul :

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.

source

ink

def Mathlib.Meta.NormNum.evalMul.core {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (e : Qq.QQ α) (a : Qq.QQ α) (b : Qq.QQ α) (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `Semiring [u]) α)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) :

Option (Mathlib.Meta.NormNum.Result e)

Main part of evalMul.

Equations

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

source

ink

theorem Mathlib.Meta.NormNum.isNat_pow {α : Type u_1} [inst : Semiring α] {a : α} {b : ℕ} {a' : ℕ} {b' : ℕ} {c : ℕ} :

Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → Nat.pow a' b' = c → Mathlib.Meta.NormNum.IsNat (a ^ b) c

source

ink

theorem Mathlib.Meta.NormNum.isInt_pow {α : Type u_1} [inst : Ring α] {a : α} {b : ℕ} {a' : ℤ} {b' : ℕ} {c : ℤ} :

Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsNat b b' → Int.pow a' b' = c → Mathlib.Meta.NormNum.IsInt (a ^ b) c

source

ink

theorem Mathlib.Meta.NormNum.isRat_pow {α : Type u_1} [inst : Ring α] {a : α} {an : ℤ} {cn : ℤ} {ad : ℕ} {b : ℕ} {b' : ℕ} {cd : ℕ} :

Mathlib.Meta.NormNum.IsRat a an ad → Mathlib.Meta.NormNum.IsNat b b' → Int.pow an b' = cn → Nat.pow ad b' = cd → Mathlib.Meta.NormNum.IsRat (a ^ b) cn cd

source

ink

def Mathlib.Meta.NormNum.evalPow :

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, with b : ℕ.

Equations

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

source

ink

def Mathlib.Meta.NormNum.evalPow.core {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (e : Qq.QQ α) (a : Qq.QQ α) (b : Q(ℕ)) (nb : Q(ℕ)) (pb : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsNat [Lean.Level.zero]) (Lean.Expr.const `Nat [])) q(Mathlib.Meta.NormNum.instAddMonoidWithOneNat)) b) nb)) (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `Semiring [u]) α)) (ra : Mathlib.Meta.NormNum.Result a) :

Option (Mathlib.Meta.NormNum.Result e)

Main part of evalPow.

Equations

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

source

ink

theorem Mathlib.Meta.NormNum.isRat_inv_pos {α : Type u_1} [inst : DivisionRing α] [inst : CharZero α] {a : α} {n : ℕ} {d : ℕ} :

Mathlib.Meta.NormNum.IsRat a (Int.ofNat (Nat.succ n)) d → Mathlib.Meta.NormNum.IsRat a⁻¹ (Int.ofNat d) (Nat.succ n)

source

ink

theorem Mathlib.Meta.NormNum.isRat_inv_one {α : Type u_1} [inst : DivisionRing α] {a : α} :

Mathlib.Meta.NormNum.IsNat a 1 → Mathlib.Meta.NormNum.IsNat a⁻¹ 1

source

ink

theorem Mathlib.Meta.NormNum.isRat_inv_zero {α : Type u_1} [inst : DivisionRing α] {a : α} :

Mathlib.Meta.NormNum.IsNat a 0 → Mathlib.Meta.NormNum.IsNat a⁻¹ 0

source

ink

theorem Mathlib.Meta.NormNum.isRat_inv_neg_one {α : Type u_1} [inst : DivisionRing α] {a : α} :

Mathlib.Meta.NormNum.IsInt a (Int.negOfNat 1) → Mathlib.Meta.NormNum.IsInt a⁻¹ (Int.negOfNat 1)

source

ink

theorem Mathlib.Meta.NormNum.isRat_inv_neg {α : Type u_1} [inst : DivisionRing α] [inst : CharZero α] {a : α} {n : ℕ} {d : ℕ} :

Mathlib.Meta.NormNum.IsRat a (Int.negOfNat (Nat.succ n)) d → Mathlib.Meta.NormNum.IsRat a⁻¹ (Int.negOfNat d) (Nat.succ n)

source

ink

def Mathlib.Meta.NormNum.evalInv :

Mathlib.Meta.NormNum.NormNumExt

The norm_num extension which identifies expressions of the form a⁻¹, such that norm_num successfully recognises a.

Equations

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

source

ink

def Mathlib.Meta.NormNum.evalInv.core {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (e : Qq.QQ α) (a : Qq.QQ α) (ra : Mathlib.Meta.NormNum.Result a) (dα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) (_i : Option (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddGroupWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Ring.toAddGroupWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toRing [u]) α) dα)))))) :

Option (Mathlib.Meta.NormNum.Result e)

Main part of evalInv.

Equations

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

source

ink

theorem Mathlib.Meta.NormNum.isRat_div {α : Type u_1} [inst : DivisionRing α] {a : α} {b : α} {cn : ℤ} {cd : ℕ} :

Mathlib.Meta.NormNum.IsRat (a * b⁻¹) cn cd → Mathlib.Meta.NormNum.IsRat (a / b) cn cd

source

ink

def Mathlib.Meta.NormNum.evalDiv :

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.

Logic #

source

ink

def Mathlib.Meta.NormNum.evalTrue :

Mathlib.Meta.NormNum.NormNumExt

The norm_num extension which identifies True.

Equations

Mathlib.Meta.NormNum.evalTrue = Mathlib.Meta.NormNum.NormNumExt.mk true true fun {u} {α} e => pure (Mathlib.Meta.NormNum.Result.isTrue q(True.intro))

source

ink

def Mathlib.Meta.NormNum.evalFalse :

Mathlib.Meta.NormNum.NormNumExt

The norm_num extension which identifies False.

Equations

Mathlib.Meta.NormNum.evalFalse = Mathlib.Meta.NormNum.NormNumExt.mk true true fun {u} {α} e => pure (Mathlib.Meta.NormNum.Result.isFalse q(not_false))

source

ink

def Mathlib.Meta.NormNum.evalNot :

Mathlib.Meta.NormNum.NormNumExt

The norm_num extension which identifies expressions of the form ¬a, such that norm_num successfully recognises a.

Equations

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

(In)equalities #

source

ink

theorem Mathlib.Meta.NormNum.isNat_eq_true {α : Type u_1} [inst : AddMonoidWithOne α] {a : α} {b : α} {a' : ℕ} {b' : ℕ} :

Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → Nat.beq a' b' = true → a = b

source

ink

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

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

source

ink

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

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

source

ink

theorem Mathlib.Meta.NormNum.isNat_eq_false {α : Type u_1} [inst : AddMonoidWithOne α] [inst : CharZero α] {a : α} {b : α} {a' : ℕ} {b' : ℕ} :

Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → Nat.beq a' b' = false → ¬a = b

source

ink

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

¬a ≤ b

source

ink

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

¬a < b

source

ink

theorem Mathlib.Meta.NormNum.isInt_eq_true {α : Type u_1} [inst : Ring α] {a : α} {b : α} {z : ℤ} :

Mathlib.Meta.NormNum.IsInt a z → Mathlib.Meta.NormNum.IsInt b z → a = b

source

ink

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

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

source

ink

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

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

source

ink

theorem Mathlib.Meta.NormNum.isInt_eq_false {α : Type u_1} [inst : Ring α] [inst : CharZero α] {a : α} {b : α} {a' : ℤ} {b' : ℤ} :

Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → decide (a' = b') = false → ¬a = b

source

ink

theorem Mathlib.Meta.NormNum.isInt_le_false {α : Type u_1} [inst : OrderedRing α] [inst : 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

ink

theorem Mathlib.Meta.NormNum.isInt_lt_false {α : Type u_1} [inst : 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

ink

theorem Mathlib.Meta.NormNum.Rat.invOf_denom_swap {α : Type u_1} [inst : Ring α] (n₁ : ℤ) (n₂ : ℤ) (a₁ : α) (a₂ : α) [inst : Invertible a₁] [inst : Invertible a₂] :

↑n₁ * ⅟a₁ = ↑n₂ * ⅟a₂ ↔ ↑n₁ * a₂ = ↑n₂ * a₁

source

ink

theorem Mathlib.Meta.NormNum.isRat_eq_true {α : Type u_1} [inst : Ring α] {a : α} {b : α} {n : ℤ} {d : ℕ} :

Mathlib.Meta.NormNum.IsRat a n d → Mathlib.Meta.NormNum.IsRat b n d → a = b

source

ink

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

Mathlib.Meta.NormNum.IsRat a na da → Mathlib.Meta.NormNum.IsRat b nb db → decide (Int.mul na (Int.ofNat db) ≤ Int.mul nb (Int.ofNat da)) = true → a ≤ b

source

ink

theorem Mathlib.Meta.NormNum.isRat_lt_true {α : Type u_1} [inst : LinearOrderedRing α] [inst : 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

ink

theorem Mathlib.Meta.NormNum.isRat_eq_false {α : Type u_1} [inst : Ring α] [inst : CharZero α] {a : α} {b : α} {na : ℤ} {nb : ℤ} {da : ℕ} {db : ℕ} :

Mathlib.Meta.NormNum.IsRat a na da → Mathlib.Meta.NormNum.IsRat b nb db → decide (Int.mul na (Int.ofNat db) = Int.mul nb (Int.ofNat da)) = false → ¬a = b

source

ink

theorem Mathlib.Meta.NormNum.isRat_le_false {α : Type u_1} [inst : LinearOrderedRing α] [inst : 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

ink

theorem Mathlib.Meta.NormNum.isRat_lt_false {α : Type u_1} [inst : 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

source

ink

theorem Mathlib.Meta.NormNum.eq_of_true {a : Prop} {b : Prop} (ha : a) (hb : b) :

a = b

source

ink

theorem Mathlib.Meta.NormNum.ne_of_false_of_true {a : Prop} {b : Prop} (ha : ¬a) (hb : b) :

a ≠ b

source

ink

theorem Mathlib.Meta.NormNum.ne_of_true_of_false {a : Prop} {b : Prop} (ha : a) (hb : ¬b) :

a ≠ b

source

ink

theorem Mathlib.Meta.NormNum.eq_of_false {a : Prop} {b : Prop} (ha : ¬a) (hb : ¬b) :

a = b

source

ink

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.

source

ink

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.

source

ink

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.

Nat operations #

source

ink

theorem Mathlib.Meta.NormNum.isNat_natSub {a : ℕ} {b : ℕ} {a' : ℕ} {b' : ℕ} {c : ℕ} :

Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → Nat.sub a' b' = c → Mathlib.Meta.NormNum.IsNat (a - b) c

source

ink

def Mathlib.Meta.NormNum.evalNatSub :

Mathlib.Meta.NormNum.NormNumExt

The norm_num extension which identifies expressions of the form Nat.sub 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.

source

ink

theorem Mathlib.Meta.NormNum.isNat_natMod {a : ℕ} {b : ℕ} {a' : ℕ} {b' : ℕ} {c : ℕ} :

Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → Nat.mod a' b' = c → Mathlib.Meta.NormNum.IsNat (a % b) c

source

ink

def Mathlib.Meta.NormNum.evalNatMod :

Mathlib.Meta.NormNum.NormNumExt

The norm_num extension which identifies expressions of the form Nat.mod 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.

norm_num basic plugins #

Logic #

(In)equalities #

Nat operations #

`norm_num` basic plugins #