zpow_right — Mathlib

English

For a square matrix A, IsUnit((A^{z}).det) holds iff IsUnit(det A) or z = 0. The determinant of a z-pow is a unit exactly in these cases.

Русский

Для матрицы A детерминант z-повторения является единичным тогда и только тогда, когда det(A) единичен или z = 0.

LaTeX

$$$$IsUnit((A^{z}).\\det) \\iff (IsUnit(A.\\det) \\lor z=0).$$$$

Lean4

theorem zpow_right {A B : M} (h : Commute A B) (m : ℤ) : Commute A (B ^ m) :=
  by
  rcases nonsing_inv_cancel_or_zero B with (⟨hB, _⟩ | hB)
  · refine SemiconjBy.zpow_right ?_ ?_ h _ <;> exact isUnit_det_of_left_inverse hB
  · cases m
    · simpa using h.pow_right _
    · simp [← inv_pow', hB]

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