# 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 : ] {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 : ] (n : ) (m : ) :

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.
theorem Mathlib.Meta.NormNum.isNat_int_cast {R : Type u_1} [inst : Ring R] (n : ) (m : ) :
theorem Mathlib.Meta.NormNum.isInt_cast {R : Type u_1} [inst : Ring R] (n : ) (m : ) :

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 : ] {a : α} {b : α} {a' : } {b' : } {c : } :
Nat.add a' b' = cMathlib.Meta.NormNum.IsNat (a + b) c
theorem Mathlib.Meta.NormNum.isInt_add {α : Type u_1} [inst : Ring α] {a : α} {b : α} {a' : } {b' : } {c : } :
Int.add a' b' = cMathlib.Meta.NormNum.IsInt (a + b) c
def Mathlib.Meta.NormNum.invertibleOfMul {α : Type u_1} [inst : ] (k : ) (b : α) (a : α) [inst : ] :
a = k * 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 : ] {a : } {k : } {b : } [inst : ] (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 : } :
Int.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.
def Mathlib.Meta.NormNum.evalAdd.core {u : Lean.Level} {α : } (e : ) (a : ) (b : ) (ra : ) (rb : ) :

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

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.evalNeg.core {u : Lean.Level} {α : } (e : ) (a : ) (ra : ) (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 : } :
Int.sub a' b' = cMathlib.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 : ) (rb : ) (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.
def Mathlib.Meta.NormNum.evalSub.core {u : Lean.Level} {α : } (e : ) (a : ) (b : ) (rα : Qq.QQ (Lean.Expr.app (Lean.Expr.const Ring [u]) α)) (ra : ) (rb : ) :

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 : ] {a : α} {b : α} {a' : } {b' : } {c : } :
Nat.mul a' b' = cMathlib.Meta.NormNum.IsNat (a * b) c
theorem Mathlib.Meta.NormNum.isInt_mul {α : Type u_1} [inst : Ring α] {a : α} {b : α} {a' : } {b' : } {c : } :
Int.mul a' b' = cMathlib.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 : } :
Int.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.
def Mathlib.Meta.NormNum.evalMul.core {u : Lean.Level} {α : } (e : ) (a : ) (b : ) (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const Semiring [u]) α)) (ra : ) (rb : ) :

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 : ] {a : α} {b : } {a' : } {b' : } {c : } :
Nat.pow a' b' = cMathlib.Meta.NormNum.IsNat (a ^ b) c
theorem Mathlib.Meta.NormNum.isInt_pow {α : Type u_1} [inst : Ring α] {a : α} {b : } {a' : } {b' : } {c : } :
Int.pow a' b' = cMathlib.Meta.NormNum.IsInt (a ^ b) c
theorem Mathlib.Meta.NormNum.isRat_pow {α : Type u_1} [inst : Ring α] {a : α} {an : } {cn : } {ad : } {b : } {b' : } {cd : } :
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.
def Mathlib.Meta.NormNum.evalPow.core {u : Lean.Level} {α : } (e : ) (a : ) (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.Expr.const Nat [])) ) b) nb)) (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const Semiring [u]) α)) (ra : ) :

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 : ] [inst : ] {a : α} {n : } {d : } :
theorem Mathlib.Meta.NormNum.isRat_inv_one {α : Type u_1} [inst : ] {a : α} :
theorem Mathlib.Meta.NormNum.isRat_inv_zero {α : Type u_1} [inst : ] {a : α} :
theorem Mathlib.Meta.NormNum.isRat_inv_neg_one {α : Type u_1} [inst : ] {a : α} :
theorem Mathlib.Meta.NormNum.isRat_inv_neg {α : Type u_1} [inst : ] [inst : ] {a : α} {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.
def Mathlib.Meta.NormNum.evalInv.core {u : Lean.Level} {α : } (e : ) (a : ) (ra : ) (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 : ] {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 True.

Equations

The norm_num extension which identifies False.

Equations

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 : ] {a : α} {b : α} {a' : } {b' : } :
Nat.beq a' b' = truea = b
theorem Mathlib.Meta.NormNum.isNat_le_true {α : Type u_1} [inst : ] {a : α} {b : α} {a' : } {b' : } :
Nat.ble a' b' = truea b
theorem Mathlib.Meta.NormNum.isNat_lt_true {α : Type u_1} [inst : ] [inst : ] {a : α} {b : α} {a' : } {b' : } :
Nat.ble b' a' = falsea < b
theorem Mathlib.Meta.NormNum.isNat_eq_false {α : Type u_1} [inst : ] [inst : ] {a : α} {b : α} {a' : } {b' : } :
Nat.beq a' b' = false¬a = b
theorem Mathlib.Meta.NormNum.isNat_le_false {α : Type u_1} [inst : ] [inst : ] {a : α} {b : α} {a' : } {b' : } (ha : ) (hb : ) (h : Nat.ble a' b' = false) :
¬a b
theorem Mathlib.Meta.NormNum.isNat_lt_false {α : Type u_1} [inst : ] {a : α} {b : α} {a' : } {b' : } (ha : ) (hb : ) (h : Nat.ble b' a' = true) :
¬a < b
theorem Mathlib.Meta.NormNum.isInt_eq_true {α : Type u_1} [inst : Ring α] {a : α} {b : α} {z : } :
a = b
theorem Mathlib.Meta.NormNum.isInt_le_true {α : Type u_1} [inst : ] {a : α} {b : α} {a' : } {b' : } :
decide (a' b') = truea b
theorem Mathlib.Meta.NormNum.isInt_lt_true {α : Type u_1} [inst : ] [inst : ] {a : α} {b : α} {a' : } {b' : } :
decide (a' < b') = truea < b
theorem Mathlib.Meta.NormNum.isInt_eq_false {α : Type u_1} [inst : Ring α] [inst : ] {a : α} {b : α} {a' : } {b' : } :
decide (a' = b') = false¬a = b
theorem Mathlib.Meta.NormNum.isInt_le_false {α : Type u_1} [inst : ] [inst : ] {a : α} {b : α} {a' : } {b' : } (ha : ) (hb : ) (h : decide (b' < a') = true) :
¬a b
theorem Mathlib.Meta.NormNum.isInt_lt_false {α : Type u_1} [inst : ] {a : α} {b : α} {a' : } {b' : } (ha : ) (hb : ) (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 : ] [inst : ] :
n₁ * a₁ = n₂ * a₂ n₁ * a₂ = n₂ * a₁
theorem Mathlib.Meta.NormNum.isRat_eq_true {α : Type u_1} [inst : Ring α] {a : α} {b : α} {n : } {d : } :
a = b
theorem Mathlib.Meta.NormNum.isRat_le_true {α : Type u_1} [inst : ] {a : α} {b : α} {na : } {nb : } {da : } {db : } :
decide (Int.mul na () Int.mul nb ()) = truea b
theorem Mathlib.Meta.NormNum.isRat_lt_true {α : Type u_1} [inst : ] [inst : ] {a : α} {b : α} {na : } {nb : } {da : } {db : } :
decide (na * db < nb * da) = truea < b
theorem Mathlib.Meta.NormNum.isRat_eq_false {α : Type u_1} [inst : Ring α] [inst : ] {a : α} {b : α} {na : } {nb : } {da : } {db : } :
decide (Int.mul na () = Int.mul nb ()) = false¬a = b
theorem Mathlib.Meta.NormNum.isRat_le_false {α : Type u_1} [inst : ] [inst : ] {a : α} {b : α} {na : } {nb : } {da : } {db : } (ha : ) (hb : ) (h : decide (nb * da < na * db) = true) :
¬a b
theorem Mathlib.Meta.NormNum.isRat_lt_false {α : Type u_1} [inst : ] {a : α} {b : α} {na : } {nb : } {da : } {db : } (ha : ) (hb : ) (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 #

theorem Mathlib.Meta.NormNum.isNat_natSub {a : } {b : } {a' : } {b' : } {c : } :
Nat.sub a' b' = cMathlib.Meta.NormNum.IsNat (a - b) c

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.
theorem Mathlib.Meta.NormNum.isNat_natMod {a : } {b : } {a' : } {b' : } {c : } :
Nat.mod a' b' = cMathlib.Meta.NormNum.IsNat (a % b) c

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.