isUnit_iff_isUnit_det

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

← MathLib Explorer

English

IsUnit A holds if and only if IsUnit det(A).

Русский

IsUnit(A) эквивалентно IsUnit(det(A)).

LaTeX

$$$\text{IsUnit}(A) \iff \text{IsUnit}(\det A)$$$

Lean4

/-- When lowered to a prop, `Matrix.invertibleEquivDetInvertible` forms an `iff`. -/
theorem isUnit_iff_isUnit_det : IsUnit A ↔ IsUnit A.det := by
  simp only [← nonempty_invertible_iff_isUnit, (invertibleEquivDetInvertible A).nonempty_congr]

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

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

Разделы

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

Аффилиация

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