det_nonsing_inv_mul_det

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

English

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

Русский

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

LaTeX

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

Lean4

theorem det_nonsing_inv_mul_det (h : IsUnit A.det) : A⁻¹.det * A.det = 1 := by
  rw [← det_mul, A.nonsing_inv_mul h, det_one]

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

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

Разделы

Аффилиация

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