English
Let A be an n×n matrix over a commutative ring R with det(A) a unit. If m and n are natural numbers and n ≤ m, then A^{m-n} = A^{m} (A^{n})^{-1}. In words, powers of A satisfy a subtraction formula when A is invertible.
Русский
Пусть A — квадратная матрица размером n×n над коммутативной кольцевой структурой R и det(A) является единичным элементом. Для натуральных чисел m, n с n ≤ m верно: A^{m-n} = A^{m} (A^{n})^{-1}. Иными словами, для A выполняется формула вычитания степеней при обратимости.
LaTeX
$$$$A^{m-n} = A^{m}\\,(A^{n})^{-1} \\quad\\text{при } \\det(A) \\in R^{\\times},\\ n \\le m.$$$$
Lean4
theorem pow_sub' (A : M) {m n : ℕ} (ha : IsUnit A.det) (h : n ≤ m) : A ^ (m - n) = A ^ m * (A ^ n)⁻¹ :=
by
rw [← tsub_add_cancel_of_le h, pow_add, Matrix.mul_assoc, mul_nonsing_inv, tsub_add_cancel_of_le h, Matrix.mul_one]
simpa using ha.pow n
