isUnit_det_transpose

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

English

If det(A) is a unit, then det(A^T) is also a unit.

Русский

Если det(A) является единицей, то det(A^T) тоже единица.

LaTeX

$$$\\det(A) \\in \\alpha^{\\times} \\Rightarrow \\det(A^T) \\in \\alpha^{\\times}$$$

Lean4

theorem isUnit_det_transpose (h : IsUnit A.det) : IsUnit Aᵀ.det :=
  by
  rw [det_transpose]
  exact h

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

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

Разделы

Аффилиация

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