English
For any square matrix A, and any nonnegative integers m, n, the inverse powers commute with the forward powers: A^{-1}^{m} A^{n} = A^{n} A^{-1}^{m}. Equivalently, A^{-m} commutes with A^{n}.
Русский
Для произвольной квадратной матрицы A и любых неотрицательных целых чисел m, n выполняется коммутативность обратных степеней и прямых степеней: A^{-1}^{m} A^{n} = A^{n} A^{-1}^{m}. Аналогично A^{-m} коммутирует с A^{n}.
LaTeX
$$$$A^{-1}^{m} A^{n} = A^{n} A^{-1}^{m}\quad(m,n\\in\\mathbb{N}).$$$$
Lean4
theorem pow_inv_comm' (A : M) (m n : ℕ) : A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m := by
induction n generalizing m with
| zero => simp
| succ n IH =>
rcases m with m | m
· simp
rcases nonsing_inv_cancel_or_zero A with ⟨h, h'⟩ | h
·
calc
A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n := by
simp only [pow_succ A⁻¹, pow_succ' A, Matrix.mul_assoc]
_ = A ^ n * A⁻¹ ^ m := by simp only [h, Matrix.mul_one, IH m]
_ = A ^ n * (A * A⁻¹) * A⁻¹ ^ m := by simp only [h', Matrix.mul_one]
_ = A ^ (n + 1) * A⁻¹ ^ (m + 1) := by simp only [pow_succ A, pow_succ' A⁻¹, Matrix.mul_assoc]
· simp [h]
