isUnit_det_of_invertible

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

URI: https://scilib.ai/kg/mathlib#Matrix.isUnit_det_of_invertible

English

If a matrix A is invertible, then det(A) is a unit in α.

Русский

Если матрица A обратима, то det(A) является единицей в α.

LaTeX

$$$\\forall A \\in \\mathrm{M}_n(\\alpha)\\, (\\text{Invertible}(A) \\Rightarrow \\det(A) \\in \\alpha^{\\times})$$$

Lean4

theorem isUnit_det_of_invertible [Invertible A] : IsUnit A.det :=
  @isUnit_of_invertible _ _ _ (detInvertibleOfInvertible A)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru