zpow_natCast — Mathlib

English

For any a ∈ G and n ∈ ℕ, a^{(n : ℤ)} = a^{n}.

Русский

Для любого a ∈ G и n ∈ ℕ, a^{(n : ℤ)} = a^{n}.

LaTeX

$$$a^{(n : \\mathbb{Z})} = a^{n}$$$

Lean4

@[to_additive (attr := simp, norm_cast) natCast_zsmul]
theorem zpow_natCast (a : G) : ∀ n : ℕ, a ^ (n : ℤ) = a ^ n
  | 0 => (zpow_zero _).trans (pow_zero _).symm
  | n + 1 =>
    calc
      a ^ (↑(n + 1) : ℤ) = a ^ (n : ℤ) * a := DivInvMonoid.zpow_succ' _ _
      _ = a ^ n * a := (congrArg (· * a) (zpow_natCast a n))
      _ = a ^ (n + 1) := (pow_succ _ _).symm

Похожие утверждения