English
For any matrix A and any integer n, with IsUnit det(A) assumed, A^{(-n)} = (A^{n})^{-1}. In other words, negative z-powers equal inverses when det is a unit.
Русский
Для любой матрицы A и любого целого n при условии, что det(A) единичен, выполняется A^{(-n)} = (A^{n})^{-1}. Отрицательные z-степени равны обратной матрице.
LaTeX
$$$$A^{(-n)} = (A^{n})^{-1} \\quad (n\\in\\mathbb{Z}, \\det(A) \\in \\mathbb{R}^{\\times}).$$$$
Lean4
theorem zpow_neg {A : M} (h : IsUnit A.det) : ∀ n : ℤ, A ^ (-n) = (A ^ n)⁻¹
| (n : ℕ) => zpow_neg_natCast _ _
| -[n+1] => by
rw [zpow_negSucc, neg_negSucc, zpow_natCast, nonsing_inv_nonsing_inv]
rw [det_pow]
exact h.pow _
