isUnits_det_units — Mathlib

English

If A is an invertible square matrix over a commutative ring α, then det(A) is a unit in α.

Русский

Пусть A — обратимая квадратная матрица над коммутативным кольцом α. Тогда det(A) является единицей в α.

LaTeX

$$$\\forall A \\in \\mathrm{GL}_n(\\alpha): \\ det(A) \\in \\alpha^{\\times}$$$

Lean4

@[simp]
theorem isUnits_det_units (A : (Matrix n n α)ˣ) : IsUnit (A : Matrix n n α).det :=
  isUnit_iff_isUnit_det _ |>.mp A.isUnit

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