specialOrthogonalGroup — Mathlib

English

The special orthogonal group is the group of orthogonal matrices with determinant one (noting this is best understood when 2 is invertible).

Русский

Специальная ортогональная группа — это группа ортогональных матриц с детерминантом равным единице (учитывая, что 2 обратимо).

LaTeX

$$$\\mathrm{specialOrthogonalGroup}(n,R) = \\mathrm{orthogonalGroup}(n,R) \\cap \\{A : \\mathrm{GL}_n(R) : \\det A = 1\\}$$$

Lean4

/-- `Matrix.specialOrthogonalGroup n` is the group of orthogonal `n` by `n` where the determinant
is one. (This definition is only correct if 2 is invertible.) -/
abbrev specialOrthogonalGroup : Submonoid (Matrix n n R) :=
  specialUnitaryGroup n R

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