Documentation

Mathlib.Tactic.NormNum.Basic

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.

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.
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.

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.

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.
theorem Mathlib.Meta.NormNum.isNat_add {α : Type u_1} [inst : AddMonoidWithOne α] {a : α} {b : α} {a' : } {b' : } {c : } :
theorem Mathlib.Meta.NormNum.isInt_add {α : Type u_1} [inst : Ring α] {a : α} {b : α} {a' : } {b' : } {c : } :
def Mathlib.Meta.NormNum.invertibleOfMul {α : Type u_1} [inst : Semiring α] (k : ) (b : α) (a : α) [inst : Invertible a] :
a = k * bInvertible 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) :

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

Equations
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 daMathlib.Meta.NormNum.IsRat b nb dbInt.add (Int.mul na db) (Int.mul nb da) = Int.mul (k) ncNat.mul da db = Nat.mul k dcMathlib.Meta.NormNum.IsRat (a + b) nc dc
Equations

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.

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 : } :
theorem Mathlib.Meta.NormNum.isRat_neg {α : Type u_1} [inst : Ring α] {a : α} {n : } {n' : } {d : } :

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.

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 : } :
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) :

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.

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 : } :
theorem Mathlib.Meta.NormNum.isInt_mul {α : Type u_1} [inst : Ring α] {a : α} {b : α} {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 daMathlib.Meta.NormNum.IsRat b nb dbInt.mul na nb = Int.mul (k) ncNat.mul da db = Nat.mul k dcMathlib.Meta.NormNum.IsRat (a * b) nc dc

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.

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 : } :
theorem Mathlib.Meta.NormNum.isInt_pow {α : Type u_1} [inst : Ring α] {a : α} {b : } {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 adMathlib.Meta.NormNum.IsNat b b'Int.pow an b' = cnNat.pow ad b' = cdMathlib.Meta.NormNum.IsRat (a ^ b) cn cd

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.

Main part of evalPow.

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

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.
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]) α) )))))) :

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 : } :

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 #

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 #

theorem Mathlib.Meta.NormNum.isNat_eq_true {α : Type u_1} [inst : AddMonoidWithOne α] {a : α} {b : α} {a' : } {b' : } :
theorem Mathlib.Meta.NormNum.isNat_le_true {α : Type u_1} [inst : OrderedSemiring α] {a : α} {b : α} {a' : } {b' : } :
theorem Mathlib.Meta.NormNum.isNat_lt_true {α : Type u_1} [inst : OrderedSemiring α] [inst : CharZero α] {a : α} {b : α} {a' : } {b' : } :
theorem Mathlib.Meta.NormNum.isNat_eq_false {α : Type u_1} [inst : AddMonoidWithOne α] [inst : CharZero α] {a : α} {b : α} {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) :
¬a b
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
theorem Mathlib.Meta.NormNum.isInt_eq_true {α : Type u_1} [inst : Ring α] {a : α} {b : α} {z : } :
theorem Mathlib.Meta.NormNum.isInt_le_true {α : Type u_1} [inst : OrderedRing α] {a : α} {b : α} {a' : } {b' : } :
theorem Mathlib.Meta.NormNum.isInt_lt_true {α : Type u_1} [inst : OrderedRing α] [inst : Nontrivial α] {a : α} {b : α} {a' : } {b' : } :
theorem Mathlib.Meta.NormNum.isInt_eq_false {α : Type u_1} [inst : Ring α] [inst : CharZero α] {a : α} {b : α} {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) :
¬a b
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
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₁
theorem Mathlib.Meta.NormNum.isRat_eq_true {α : Type u_1} [inst : Ring α] {a : α} {b : α} {n : } {d : } :
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 daMathlib.Meta.NormNum.IsRat b nb dbdecide (na * db < nb * da) = truea < b
theorem Mathlib.Meta.NormNum.isRat_eq_false {α : Type u_1} [inst : Ring α] [inst : CharZero α] {a : α} {b : α} {na : } {nb : } {da : } {db : } :
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
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
theorem Mathlib.Meta.NormNum.eq_of_true {a : Prop} {b : Prop} (ha : a) (hb : b) :
a = b
theorem Mathlib.Meta.NormNum.ne_of_false_of_true {a : Prop} {b : Prop} (ha : ¬a) (hb : b) :
a b
theorem Mathlib.Meta.NormNum.ne_of_true_of_false {a : Prop} {b : Prop} (ha : a) (hb : ¬b) :
a b
theorem Mathlib.Meta.NormNum.eq_of_false {a : Prop} {b : Prop} (ha : ¬a) (hb : ¬b) :
a = b

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.

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.

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 #

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.

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.