zpow_one_add — Mathlib

English

For a square matrix A with det(A) a unit, A^{1+m} = A A^{m} for all integers m.

Русский

Для квадратной матрицы A с единичным детерминантным составом, A^{1+m} = A A^{m} для всех целых m.

LaTeX

$$$$A^{1+m} = A A^{m} \\quad (m\\in\\mathbb{Z}), \\det(A) \\in \\mathbb{R}^{\\times}.$$$$

Lean4

theorem zpow_one_add {A : M} (h : IsUnit A.det) (i : ℤ) : A ^ (1 + i) = A * A ^ i := by rw [zpow_add h, zpow_one]

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