zpow_add_of_nonneg — Mathlib

English

If both m and n are nonnegative, then A^{m+n} = A^{m} A^{n} for a square matrix A (with det(A) a unit).

Русский

Если обе величины m и n неотрицательны, то A^{m+n} = A^{m} A^{n} для квадратной матрицы A с единичным детерминантом.

LaTeX

$$$$A^{m+n} = A^{m} A^{n} \\quad (m,n\\ge 0), \\det(A)\\in \\mathbb{R}^{\\times}.$$$$

Lean4

theorem zpow_add_of_nonneg {A : M} {m n : ℤ} (hm : 0 ≤ m) (hn : 0 ≤ n) : A ^ (m + n) = A ^ m * A ^ n :=
  by
  obtain ⟨k, rfl⟩ := eq_ofNat_of_zero_le hm
  obtain ⟨l, rfl⟩ := eq_ofNat_of_zero_le hn
  rw [← Int.natCast_add, zpow_natCast, zpow_natCast, zpow_natCast, pow_add]

Похожие утверждения