zpow_sub_one₀ — Mathlib

English

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

Русский

Если a ≠ 0, то для любого целого n: a^{n-1} = a^{n} · a^{-1}.

LaTeX

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

Lean4

theorem zpow_sub_one₀ (ha : a ≠ 0) (n : ℤ) : a ^ (n - 1) = a ^ n * a⁻¹ :=
  calc
    a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹ := by rw [mul_assoc, mul_inv_cancel₀ ha, mul_one]
    _ = a ^ n * a⁻¹ := by rw [← zpow_add_one₀ ha, Int.sub_add_cancel]

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