norm_num basic plugins #
This file adds norm_num plugins for
- constructors and constants
Nat.cast,Int.cast, andmkRat+,-,*, and/Nat.succ,Nat.sub,Nat.mod, andNat.div.
See other files in this directory for many more plugins.
Constructors and constants #
theorem
Mathlib.Meta.NormNum.isNat_zero
(α : Type u_1)
[AddMonoidWithOne α]
:
Mathlib.Meta.NormNum.IsNat Zero.zero 0
theorem
Mathlib.Meta.NormNum.isNat_one
(α : Type u_1)
[AddMonoidWithOne α]
:
Mathlib.Meta.NormNum.IsNat One.one 1
theorem
Mathlib.Meta.NormNum.isNat_ofNat
(α : Type u_1)
[AddMonoidWithOne α]
{a : α}
{n : ℕ}
(h : ↑n = a)
:
The norm_num extension which identifies an expression OfNat.ofNat n, returning n.
theorem
Mathlib.Meta.NormNum.isNat_intOfNat
{n : ℕ}
{n' : ℕ}
:
Mathlib.Meta.NormNum.IsNat n n' → Mathlib.Meta.NormNum.IsNat (Int.ofNat n) n'
The norm_num extension which identifies the expression Int.natAbs n such that
norm_num successfully recognizes n.
Equations
- One or more equations did not get rendered due to their size.
Casts #
theorem
Mathlib.Meta.NormNum.isNat_cast
{R : Type u_1}
[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}
[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}
[Ring R]
(n : ℤ)
(m : ℤ)
:
Mathlib.Meta.NormNum.IsInt n m → Mathlib.Meta.NormNum.IsInt (↑n) m
Arithmetic #
theorem
Mathlib.Meta.NormNum.isNat_add
{α : Type u_1}
[AddMonoidWithOne α]
{f : α → α → α}
{a : α}
{b : α}
{a' : ℕ}
{b' : ℕ}
{c : ℕ}
:
f = HAdd.hAdd →
Mathlib.Meta.NormNum.IsNat a a' →
Mathlib.Meta.NormNum.IsNat b b' → Nat.add a' b' = c → Mathlib.Meta.NormNum.IsNat (f a b) c
theorem
Mathlib.Meta.NormNum.isInt_add
{α : Type u_1}
[Ring α]
{f : α → α → α}
{a : α}
{b : α}
{a' : ℤ}
{b' : ℤ}
{c : ℤ}
:
f = HAdd.hAdd →
Mathlib.Meta.NormNum.IsInt a a' →
Mathlib.Meta.NormNum.IsInt b b' → Int.add a' b' = c → Mathlib.Meta.NormNum.IsInt (f a b) c
def
Mathlib.Meta.NormNum.invertibleOfMul
{α : Type u_1}
[Semiring α]
(k : ℕ)
(b : α)
(a : α)
[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}
[Semiring α]
{a : ℕ}
{k : ℕ}
{b : ℕ}
[Invertible ↑a]
(h : a = k * b)
:
Invertible ↑b
If b divides a and a is invertible, then b is invertible.
Equations
theorem
Mathlib.Meta.NormNum.isRat_add
{α : Type u_1}
[Ring α]
{f : α → α → α}
{a : α}
{b : α}
{na : ℤ}
{nb : ℤ}
{nc : ℤ}
{da : ℕ}
{db : ℕ}
{dc : ℕ}
{k : ℕ}
:
f = HAdd.hAdd →
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 (f a b) nc dc
def
Mathlib.Meta.NormNum.evalAdd.core
{u : Lean.Level}
{α : Q(Type u)}
(e : Q(«$α»))
(f : Q(«$α» → «$α» → «$α»))
(a : Q(«$α»))
(b : Q(«$α»))
(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.
def
Mathlib.Meta.NormNum.evalAdd.core.intArm
{u : Lean.Level}
{α : Q(Type u)}
(e : Q(«$α»))
(f : Q(«$α» → «$α» → «$α»))
(a : Q(«$α»))
(b : Q(«$α»))
(ra : Mathlib.Meta.NormNum.Result a)
(rb : Mathlib.Meta.NormNum.Result b)
(rα : Q(Ring «$α»))
:
Equations
- One or more equations did not get rendered due to their size.
def
Mathlib.Meta.NormNum.evalAdd.core.ratArm
{u : Lean.Level}
{α : Q(Type u)}
(e : Q(«$α»))
(f : Q(«$α» → «$α» → «$α»))
(a : Q(«$α»))
(b : Q(«$α»))
(ra : Mathlib.Meta.NormNum.Result a)
(rb : Mathlib.Meta.NormNum.Result b)
(dα : Q(DivisionRing «$α»))
:
Equations
- One or more equations did not get rendered due to their size.
theorem
Mathlib.Meta.NormNum.isInt_neg
{α : Type u_1}
[Ring α]
{f : α → α}
{a : α}
{a' : ℤ}
{b : ℤ}
:
f = Neg.neg → 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}
[Ring α]
{f : α → α}
{a : α}
{n : ℤ}
{n' : ℤ}
{d : ℕ}
:
f = Neg.neg → 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}
{α : Q(Type u)}
(e : Q(«$α»))
(f : Q(«$α» → «$α»))
(a : Q(«$α»))
(ra : Mathlib.Meta.NormNum.Result a)
(rα : Q(Ring «$α»))
:
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}
[Ring α]
{f : α → α → α}
{a : α}
{b : α}
{a' : ℤ}
{b' : ℤ}
{c : ℤ}
:
f = HSub.hSub →
Mathlib.Meta.NormNum.IsInt a a' →
Mathlib.Meta.NormNum.IsInt b b' → Int.sub a' b' = c → Mathlib.Meta.NormNum.IsInt (f a b) c
theorem
Mathlib.Meta.NormNum.isRat_sub
{α : Type u_1}
[Ring α]
{f : α → α → α}
{a : α}
{b : α}
{na : ℤ}
{nb : ℤ}
{nc : ℤ}
{da : ℕ}
{db : ℕ}
{dc : ℕ}
{k : ℕ}
(hf : f = HSub.hSub)
(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 (f a b) nc dc
def
Mathlib.Meta.NormNum.evalSub.core
{u : Lean.Level}
{α : Q(Type u)}
(e : Q(«$α»))
(f : Q(«$α» → «$α» → «$α»))
(a : Q(«$α»))
(b : Q(«$α»))
(rα : Q(Ring «$α»))
(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}
[Semiring α]
{f : α → α → α}
{a : α}
{b : α}
{a' : ℕ}
{b' : ℕ}
{c : ℕ}
:
f = HMul.hMul →
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}
[Ring α]
{f : α → α → α}
{a : α}
{b : α}
{a' : ℤ}
{b' : ℤ}
{c : ℤ}
:
f = HMul.hMul →
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}
[Ring α]
{f : α → α → α}
{a : α}
{b : α}
{na : ℤ}
{nb : ℤ}
{nc : ℤ}
{da : ℕ}
{db : ℕ}
{dc : ℕ}
{k : ℕ}
:
f = HMul.hMul →
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 (f a b) nc dc
def
Mathlib.Meta.NormNum.evalMul.core
{u : Lean.Level}
{α : Q(Type u)}
(e : Q(«$α»))
(f : Q(«$α» → «$α» → «$α»))
(a : Q(«$α»))
(b : Q(«$α»))
(sα : Q(Semiring «$α»))
(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.
def
Mathlib.Meta.NormNum.evalMul.core.intArm
{u : Lean.Level}
{α : Q(Type u)}
(e : Q(«$α»))
(f : Q(«$α» → «$α» → «$α»))
(a : Q(«$α»))
(b : Q(«$α»))
(sα : Q(Semiring «$α»))
(ra : Mathlib.Meta.NormNum.Result a)
(rb : Mathlib.Meta.NormNum.Result b)
(rα : Q(Ring «$α»))
:
Equations
- One or more equations did not get rendered due to their size.
def
Mathlib.Meta.NormNum.evalMul.core.ratArm
{u : Lean.Level}
{α : Q(Type u)}
(e : Q(«$α»))
(f : Q(«$α» → «$α» → «$α»))
(a : Q(«$α»))
(b : Q(«$α»))
(sα : Q(Semiring «$α»))
(ra : Mathlib.Meta.NormNum.Result a)
(rb : Mathlib.Meta.NormNum.Result b)
(dα : Q(DivisionRing «$α»))
:
Equations
- One or more equations did not get rendered due to their size.
theorem
Mathlib.Meta.NormNum.isRat_div
{α : Type u_1}
[DivisionRing α]
{a : α}
{b : α}
{cn : ℤ}
{cd : ℕ}
:
Mathlib.Meta.NormNum.IsRat (a * b⁻¹) cn cd → Mathlib.Meta.NormNum.IsRat (a / b) cn cd
def
Mathlib.Meta.NormNum.inferDivisionRing
{u : Lean.Level}
(α : Q(Type u))
:
Lean.MetaM Q(DivisionRing «$α»)
Helper function to synthesize a typed DivisionRing α expression.
Equations
- One or more equations did not get rendered due to their size.
Logic #
(In)equalities #
theorem
Mathlib.Meta.NormNum.isNat_eq_true
{α : Type u_1}
[AddMonoidWithOne α]
{a : α}
{b : α}
{c : ℕ}
:
Mathlib.Meta.NormNum.IsNat a c → Mathlib.Meta.NormNum.IsNat b c → a = b
theorem
Mathlib.Meta.NormNum.isInt_eq_true
{α : Type u_1}
[Ring α]
{a : α}
{b : α}
{z : ℤ}
:
Mathlib.Meta.NormNum.IsInt a z → Mathlib.Meta.NormNum.IsInt b z → a = b
theorem
Mathlib.Meta.NormNum.isRat_eq_true
{α : Type u_1}
[Ring α]
{a : α}
{b : α}
{n : ℤ}
{d : ℕ}
:
Mathlib.Meta.NormNum.IsRat a n d → Mathlib.Meta.NormNum.IsRat b n d → a = b
Nat operations #
theorem
Mathlib.Meta.NormNum.isNat_natSucc
{a : ℕ}
{a' : ℕ}
{c : ℕ}
:
Mathlib.Meta.NormNum.IsNat a a' → Nat.succ a' = c → Mathlib.Meta.NormNum.IsNat (Nat.succ a) c
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
theorem
Mathlib.Meta.NormNum.isNat_natDiv
{a : ℕ}
{b : ℕ}
{a' : ℕ}
{b' : ℕ}
{c : ℕ}
:
Mathlib.Meta.NormNum.IsNat a a' →
Mathlib.Meta.NormNum.IsNat b b' → Nat.div a' b' = c → Mathlib.Meta.NormNum.IsNat (a / b) c
theorem
Mathlib.Meta.NormNum.isNat_dvd_true
{a : ℕ}
{b : ℕ}
{a' : ℕ}
{b' : ℕ}
:
Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → Nat.mod b' a' = 0 → a ∣ b
theorem
Mathlib.Meta.NormNum.isNat_dvd_false
{a : ℕ}
{b : ℕ}
{a' : ℕ}
{b' : ℕ}
{c : ℕ}
:
Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → Nat.mod b' a' = Nat.succ c → ¬a ∣ b