zpow_add_one₀ — Mathlib

English

If a ≠ 0, then for every integer n, a^{n+1} = a^{n} · a.

Русский

Если a ≠ 0, то для любого целого n выполняется a^{n+1} = a^{n} · a.

LaTeX

$$$a \\\\neq 0 \\\\rightarrow \\\\forall n \\\\in \\\\mathbb{Z}, a^{n+1} = a^{n} \\\\cdot a$$$

Lean4

theorem zpow_add_one₀ (ha : a ≠ 0) : ∀ n : ℤ, a ^ (n + 1) = a ^ n * a
  | (n : ℕ) => by simp only [← Int.natCast_succ, zpow_natCast, pow_succ]
  | -1 => by simp [ha]
  | .negSucc (n + 1) => by
    rw [Int.negSucc_eq, zpow_neg, Int.neg_add, Int.neg_add_cancel_right, zpow_neg, ← Int.natCast_succ, zpow_natCast,
      zpow_natCast, pow_succ' _ (n + 1), mul_inv_rev, mul_assoc, inv_mul_cancel₀ ha, mul_one]

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