English
For a square matrix A with det(A) a unit, A^{m+n} = A^{m} A^{n} for all integers m,n. This generalizes the exponent addition rule to z-powers.
Русский
Для квадратной матрицы A с детерминантом единичного типа верно A^{m+n} = A^{m} A^{n} для любых целых m,n.
LaTeX
$$$$A^{m+n} = A^{m} A^{n} \\quad (m,n\\in\\mathbb{Z}), \\det(A) \\in \\mathbb{R}^{\\times}.$$$$
Lean4
theorem zpow_add {A : M} (ha : IsUnit A.det) (m n : ℤ) : A ^ (m + n) = A ^ m * A ^ n := by
induction n with
| zero => simp
| succ n ihn => simp only [← add_assoc, zpow_add_one ha, ihn, mul_assoc]
| pred n ihn => rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]
