mem_orthogonalGroup_iff

Mathlib.LinearAlgebra.UnitaryGroup

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

English

An element A lies in the orthogonal group iff AᵀA = I.

Русский

Элемент A принадлежит ортогональной группе тогда и только тогда, когда AᵀA = I.

LaTeX

$$$A \\in \\mathrm{orthogonalGroup}(n,R) \\iff A^{\\top}A = I$$$

Lean4

theorem mem_orthogonalGroup_iff {A : Matrix n n R} : A ∈ Matrix.orthogonalGroup n R ↔ A * Aᵀ = 1 :=
  mem_unitaryGroup_iff

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

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

Разделы

Аффилиация

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