detInvertibleOfInvertible

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

← MathLib Explorer

English

If A is invertible, then det(A) is invertible.

Русский

Если A обратима, то det(A) обратим.

LaTeX

$$$A \text{ invertible } \Rightarrow \det(A) \text{ invertible}$$$

Lean4

/-- If `A` has a constructive inverse, produce one for `A.det`. -/
def detInvertibleOfInvertible [Invertible A] : Invertible A.det :=
  detInvertibleOfLeftInverse A (⅟A) (invOf_mul_self _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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