hasOrthogonalRows

Mathlib.LinearAlgebra.Matrix.Orthogonal

URI: https://scilib.ai/kg/mathlib#Matrix.HasOrthogonalCols.hasOrthogonalRows

English

If Aᵀ has orthogonal rows, then A has orthogonal columns.

Русский

Если Aᵀ имеет ортогональные строки, то у A ортогональные столбцы.

LaTeX

$$$A^{\top}.HasOrthogonalRows \Rightarrow A.HasOrthogonalCols$$$

Lean4

theorem hasOrthogonalRows [Fintype n] (h : Aᵀ.HasOrthogonalCols) : A.HasOrthogonalRows :=
  h

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

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

Разделы

Аффилиация

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