English
Let A be a square matrix over a commutative ring R. For every integer n with n ≠ -1, the z-powers satisfy A^(n+1) = A^n A.
Русский
Пусть A — квадратная матрица над коммутативным кольцом R. Для любого целого числа n, удовлетворяющего n ≠ -1, выполняется A^(n+1) = A^n A.
LaTeX
$$$ \forall n \in \mathbb{Z},\ n \neq -1 \Rightarrow A^{n+1} = A^n A $$$
Lean4
theorem zpow_add_one_of_ne_neg_one {A : M} : ∀ n : ℤ, n ≠ -1 → A ^ (n + 1) = A ^ n * A
| (n : ℕ), _ => by simp only [pow_succ, ← Nat.cast_succ, zpow_natCast]
| -1, h => absurd rfl h
| -((n : ℕ) + 2), _ => by
rcases nonsing_inv_cancel_or_zero A with (⟨h, _⟩ | h)
· apply zpow_add_one (isUnit_det_of_left_inverse h)
· change A ^ (-((n + 1 : ℕ) : ℤ)) = A ^ (-((n + 2 : ℕ) : ℤ)) * A
simp_rw [zpow_neg_natCast, ← inv_pow', h, zero_pow <| Nat.succ_ne_zero _, zero_mul]
