norm_num
basic plugins #
This file adds norm_num
plugins for +
, *
and ^
along with other basic operations.
theorem
Mathlib.Meta.NormNum.isNat_zero
(α : Type u_1)
[inst : AddMonoidWithOne α]
:
Mathlib.Meta.NormNum.IsNat Zero.zero 0
theorem
Mathlib.Meta.NormNum.isNat_one
(α : Type u_1)
[inst : AddMonoidWithOne α]
:
Mathlib.Meta.NormNum.IsNat One.one 1
theorem
Mathlib.Meta.NormNum.isNat_ofNat
(α : Type u_1)
[inst : AddMonoidWithOne α]
{a : α}
{n : ℕ}
(h : ↑n = a)
:
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.
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
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
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
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
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
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.
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)
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
Equations
- Mathlib.Meta.NormNum.instMonadLiftOptionMetaM = { monadLift := fun {α} x => match x with | none => failure | some e => pure e }
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)
:
Main part of evalAdd
.
Equations
- One or more equations did not get rendered due to their size.
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
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
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]) α))
:
Main part of evalNeg
.
Equations
- One or more equations did not get rendered due to their size.
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
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
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)
:
Main part of evalAdd
.
Equations
- One or more equations did not get rendered due to their size.
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
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
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
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)
:
Main part of evalMul
.
Equations
- One or more equations did not get rendered due to their size.
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
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
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
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)
:
Main part of evalPow
.
Equations
- One or more equations did not get rendered due to their size.
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)
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)
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α))))))
:
Main part of evalInv
.
Equations
- One or more equations did not get rendered due to their size.
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
Logic #
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))
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))
(In)equalities #
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
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
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
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
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)
:
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)
:
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
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
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
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)
:
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)
:
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
theorem
Mathlib.Meta.NormNum.isRat_le_true
{α : Type u_1}
[inst : LinearOrderedRing α]
{a : α}
{b : α}
{na : ℤ}
{nb : ℤ}
{da : ℕ}
{db : ℕ}
:
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
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)
:
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)
:
Nat operations #
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
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