isUnit_nonsing_inv_iff

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

← MathLib Explorer

English

IsUnit A⁻¹ ↔ IsUnit A.

Русский

IsUnit A⁻¹ ⇔ IsUnit A.

LaTeX

$$$IsUnit(A^{-1}) \iff IsUnit(A).$$$

Lean4

@[simp]
theorem isUnit_nonsing_inv_iff {A : Matrix n n α} : IsUnit A⁻¹ ↔ IsUnit A := by
  simp_rw [isUnit_iff_isUnit_det, isUnit_nonsing_inv_det_iff]
    -- `IsUnit.invertible` lifts the proposition `IsUnit A` to a constructive inverse of `A`.

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

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

Разделы

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

Аффилиация

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