mem_orthogonalGroup_iff' — Mathlib

English

An element A lies in the orthogonal group iff AᵀA = I (transpose form).

Русский

Элемент 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'

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