zpow_add₀ — Mathlib

English

If a ≠ 0, then for all integers m,n, a^{m+n} = a^{m} · a^{n}.

Русский

Если a ≠ 0, то для любых целых m,n: a^{m+n} = a^{m} · a^{n}.

LaTeX

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

Lean4

theorem zpow_add₀ (ha : a ≠ 0) (m n : ℤ) : a ^ (m + n) = a ^ m * a ^ n := by
  induction n with
  | zero => simp
  | succ n ihn => simp only [← Int.add_assoc, zpow_add_one₀ ha, ihn, mul_assoc]
  | pred n ihn => rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, Int.add_sub_assoc]

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