det_zpow — Mathlib

English

If det(A) is a unit, then for every integer n, det(A^{n}) is a unit. The unit-ness of the determinant is preserved under z-powers.

Русский

Если det(A) является единичным элементом, то для каждого целого n детерминант A^{n} является единичным. Единичность детерминанта сохраняется под z-повышениями.

LaTeX

$$$$\\det(A) \\in \\mathbb{R}^{\\times} \\implies \\det(A^{n}) \\in \\mathbb{R}^{\\times} \\quad (n \\in \\mathbb{Z}).$$$$

Lean4

theorem _root_.IsUnit.det_zpow {A : M} (h : IsUnit A.det) (n : ℤ) : IsUnit (A ^ n).det :=
  by
  rcases n with n | n
  · simpa using h.pow n
  · simpa using h.pow n.succ

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