isUnit_nonsing_inv_det

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

English

If A.det is a unit, then det(A⁻¹) is a unit.

Русский

Если det A является единицей, то det(A⁻¹) является единицей.

LaTeX

$$$\text{If } \det A \in R^{\times}, \; \det(A^{-1}) \in R^{\times}.$$$

Lean4

theorem isUnit_nonsing_inv_det (h : IsUnit A.det) : IsUnit A⁻¹.det :=
  isUnit_of_mul_eq_one _ _ (A.det_nonsing_inv_mul_det h)

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

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

Разделы

Аффилиация

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