English
If det(A) is a unit, then A^{n+1} = A^{n} A for all integers n. This is the standard recursion for z-powers.
Русский
Если det(A) единичен, то A^{n+1} = A^{n} A для всех целых n. Это обычное рекурсивное свойство z-повторений.
LaTeX
$$$$A^{n+1} = A^{n} A \\quad (n\\in\\mathbb{Z}), \\det(A) \\in \\mathbb{R}^{\\times}.$$$$
Lean4
theorem zpow_add_one {A : M} (h : IsUnit A.det) : ∀ n : ℤ, A ^ (n + 1) = A ^ n * A
| (n : ℕ) => by simp only [← Nat.cast_succ, pow_succ, zpow_natCast]
| -[n+1] =>
calc
A ^ (-(n + 1) + 1 : ℤ) = (A ^ n)⁻¹ := by rw [neg_add, neg_add_cancel_right, zpow_neg h, zpow_natCast]
_ = (A * A ^ n)⁻¹ * A := by rw [mul_inv_rev, Matrix.mul_assoc, nonsing_inv_mul _ h, Matrix.mul_one]
_ = A ^ (-(n + 1 : ℤ)) * A := by rw [zpow_neg h, ← Int.natCast_succ, zpow_natCast, pow_succ']
