zpow_sub_one — Mathlib

English

If det(A) is a unit, then A^{n-1} = A^{n} A^{-1} for all integers n. This is the backward step formula for z-powers.

Русский

Если det(A) единичен, то A^{n-1} = A^{n} A^{-1} для всех целых n. Это обратная формула шага по z-порядку степеней.

LaTeX

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

Lean4

theorem zpow_sub_one {A : M} (h : IsUnit A.det) (n : ℤ) : A ^ (n - 1) = A ^ n * A⁻¹ :=
  calc
    A ^ (n - 1) = A ^ (n - 1) * A * A⁻¹ := by rw [mul_assoc, mul_nonsing_inv _ h, mul_one]
    _ = A ^ n * A⁻¹ := by rw [← zpow_add_one h, sub_add_cancel]

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