norm_num plugin for ^.

theorem Mathlib.Meta.NormNum.natPow_zero {a : ℕ} : Nat.pow a 0 = 1

theorem Mathlib.Meta.NormNum.natPow_one {a : ℕ} : Nat.pow a 1 = a

theorem Mathlib.Meta.NormNum.zero_natPow {b : ℕ} : Nat.pow 0 (Nat.succ b) = 0

theorem Mathlib.Meta.NormNum.one_natPow {b : ℕ} : Nat.pow 1 b = 1

structure Mathlib.Meta.NormNum.IsNatPowT (p : Prop) (a : ℕ) (b : ℕ) (c : ℕ) : Prop

• run' : p → Nat.pow a b = c

  Unfolds the assertion.

This is an opaque wrapper around Nat.pow to prevent lean from unfolding the definition of Nat.pow on numerals. The arbitrary precondition p is actually a formula of the form Nat.pow a' b' = c' but we usually don't care to unfold this proposition so we just carry a reference to it.

theorem Mathlib.Meta.NormNum.IsNatPowT.run {a : ℕ} {b : ℕ} {c : ℕ} (p : Mathlib.Meta.NormNum.IsNatPowT (Nat.pow a 1 = a) a b c) : Nat.pow a b = c

theorem Mathlib.Meta.NormNum.IsNatPowT.trans {p : Prop} {a : ℕ} {b : ℕ} {c : ℕ} {b' : ℕ} {c' : ℕ} (h1 : Mathlib.Meta.NormNum.IsNatPowT p a b c) (h2 : Mathlib.Meta.NormNum.IsNatPowT (Nat.pow a b = c) a b' c') : Mathlib.Meta.NormNum.IsNatPowT p a b' c'

This is the key to making the proof proceed as a balanced tree of applications instead of a linear sequence. It is just modus ponens after unwrapping the definitions.

theorem Mathlib.Meta.NormNum.IsNatPowT.bit0 {a : ℕ} {b : ℕ} {c : ℕ} : Mathlib.Meta.NormNum.IsNatPowT (Nat.pow a b = c) a (2 * b) (Nat.mul c c)

theorem Mathlib.Meta.NormNum.IsNatPowT.bit1 {a : ℕ} {b : ℕ} {c : ℕ} : Mathlib.Meta.NormNum.IsNatPowT (Nat.pow a b = c) a (2 * b + 1) (Nat.mul c (Nat.mul c a))

theorem Mathlib.Meta.NormNum.intPow_ofNat {a : ℕ} {b : ℕ} {c : ℕ} (h1 : Nat.pow a b = c) : Int.pow (Int.ofNat a) b = Int.ofNat c

theorem Mathlib.Meta.NormNum.intPow_negOfNat_bit0 {a : ℕ} {b' : ℕ} {c' : ℕ} {b : ℕ} {c : ℕ} (h1 : Nat.pow a b' = c') (hb : 2 * b' = b) (hc : c' * c' = c) : Int.pow (Int.negOfNat a) b = Int.ofNat c

theorem Mathlib.Meta.NormNum.intPow_negOfNat_bit1 {a : ℕ} {b' : ℕ} {c' : ℕ} {b : ℕ} {c : ℕ} (h1 : Nat.pow a b' = c') (hb : 2 * b' + 1 = b) (hc : c' * (c' * a) = c) : Int.pow (Int.negOfNat a) b = Int.negOfNat c

theorem Mathlib.Meta.NormNum.isNat_pow {α : Type u_1} [Semiring α] {f : α → ℕ → α} {a : α} {b : ℕ} {a' : ℕ} {b' : ℕ} {c : ℕ} : f = HPow.hPow → Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → Nat.pow a' b' = c → Mathlib.Meta.NormNum.IsNat (f a b) c

theorem Mathlib.Meta.NormNum.isInt_pow {α : Type u_1} [Ring α] {f : α → ℕ → α} {a : α} {b : ℕ} {a' : ℤ} {b' : ℕ} {c : ℤ} : f = HPow.hPow → Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsNat b b' → Int.pow a' b' = c → Mathlib.Meta.NormNum.IsInt (f a b) c

theorem Mathlib.Meta.NormNum.isRat_pow {α : Type u_1} [Ring α] {f : α → ℕ → α} {a : α} {an : ℤ} {cn : ℤ} {ad : ℕ} {b : ℕ} {b' : ℕ} {cd : ℕ} : f = HPow.hPow → 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 (f a b) cn cd

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.