English
If both m and n are nonpositive, then A^{m+n} = A^{m} A^{n} for a square matrix A with det(A) a unit. The result follows from the inverse powers in the nonpositive regime.
Русский
Если обе величины m и n не положительны, то A^{m+n} = A^{m} A^{n} для квадратной матрицы A с единичным детерминантом.
LaTeX
$$$$A^{m+n} = A^{m} A^{n} \\quad (m,n\\le 0), \\det(A)\\in \\mathbb{R}^{\\times}.$$$$
Lean4
theorem zpow_add_of_nonpos {A : M} {m n : ℤ} (hm : m ≤ 0) (hn : n ≤ 0) : A ^ (m + n) = A ^ m * A ^ n :=
by
rcases nonsing_inv_cancel_or_zero A with (⟨h, _⟩ | h)
· exact zpow_add (isUnit_det_of_left_inverse h) m n
· obtain ⟨k, rfl⟩ := exists_eq_neg_ofNat hm
obtain ⟨l, rfl⟩ := exists_eq_neg_ofNat hn
simp_rw [← neg_add, ← Int.natCast_add, zpow_neg_natCast, ← inv_pow', h, pow_add]
