Documentation

Atlas.AlgebraNotes.code.OrthogonalGroup

source
@[implicit_reducible]
instance OrthogonalGroup.orthogonalGroup_group {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommRing R] :
Group ↥(Matrix.orthogonalGroup n R)
source
def OrthogonalGroup.toGL {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommRing R] :
↥(Matrix.orthogonalGroup n R) →* GL n R
Instances For
    source
    def OrthogonalGroup.orthogonalSubgroup (n : Type u_3) [DecidableEq n] [Fintype n] (R : Type u_4) [CommRing R] :
    Subgroup (GL n R)
    Instances For
      source
      def OrthogonalGroup.specialOrthogonalSubgroup {n : Type u_1} [DecidableEq n] [Fintype n] :
      Subgroup ↥(Matrix.orthogonalGroup n ℝ)
      Instances For