English
Let A be a square matrix with det(A) a unit (i.e., A is invertible). Then for all integers m,n, A^(m n) = (A^m)^n.
Русский
Пусть A — квадратная матрица, детерминант которой является обратимым (A обратима). Тогда для любых целых m,n выполняется A^(m n) = (A^m)^n.
LaTeX
$$$ \det(A) \text{ is a unit } \Rightarrow \forall m,n \in \mathbb{Z},\ A^{m n} = (A^m)^n $$$
Lean4
theorem zpow_mul (A : M) (h : IsUnit A.det) : ∀ m n : ℤ, A ^ (m * n) = (A ^ m) ^ n
| (m : ℕ), (n : ℕ) => by rw [zpow_natCast, zpow_natCast, ← pow_mul, ← zpow_natCast, Int.natCast_mul]
| (m : ℕ), -[n+1] => by rw [zpow_natCast, zpow_negSucc, ← pow_mul, ofNat_mul_negSucc, zpow_neg_natCast]
| -[m+1], (n : ℕ) => by
rw [zpow_natCast, zpow_negSucc, ← inv_pow', ← pow_mul, negSucc_mul_ofNat, zpow_neg_natCast, inv_pow']
| -[m+1], -[n+1] =>
by
rw [zpow_negSucc, zpow_negSucc, negSucc_mul_negSucc, ← Int.natCast_mul, zpow_natCast, inv_pow', ← pow_mul,
nonsing_inv_nonsing_inv]
rw [det_pow]
exact h.pow _
