isUnit_det_of_left_inverse

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

English

If B is a left inverse of A (i.e., B A = I), then det(A) is a unit.

Русский

Если у A существует левый обратный B (BA = I), тогда det(A) является единицей.

LaTeX

$$$\\forall A,B:\\ BA=I_n \\Rightarrow \\det(A) \\in \\alpha^{\\times}$$$

Lean4

theorem isUnit_det_of_left_inverse (h : B * A = 1) : IsUnit A.det :=
  @isUnit_of_invertible _ _ _ (detInvertibleOfLeftInverse _ _ h)

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

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

Разделы

Аффилиация

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