isUnit_transpose

Mathlib.Data.Matrix.Invertible

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

← MathLib Explorer

English

IsUnit is preserved under transpose: IsUnit(A^T) iff IsUnit(A).

Русский

IsUnit сохраняется под транспонированием: IsUnit(A^T) ⇔ IsUnit(A).

LaTeX

$$$\text{IsUnit}(A^{T}) \iff \text{IsUnit}(A)$$$

Lean4

@[simp]
theorem isUnit_transpose : IsUnit Aᵀ ↔ IsUnit A := by
  simp only [← nonempty_invertible_iff_isUnit, (transposeInvertibleEquivInvertible A).nonempty_congr]

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

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

Разделы

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

Аффилиация

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