det_isUnit — Mathlib

English

The determinant of a unitary matrix is a unit (invertible) element of the base ring α.

Русский

Определитель унитарной матрицы является обратимым элементом базового кольца α.

LaTeX

$$$\\det(A) \\in \\alpha^{\\times}$ for $A \\in \\mathrm{unitaryGroup}(n,\\alpha)$.$$

Lean4

@[simp]
theorem det_isUnit (A : unitaryGroup n α) : IsUnit (A : Matrix n n α).det :=
  isUnit_iff_isUnit_det _ |>.mp <| (unitary.toUnits A).isUnit

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