Theorems · Definition · group theory

Matrix.specialUnitaryGroup

(n : Type u) →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] → (α : Type v) → [inst_2 : CommRing α] → [StarRing α] → Submonoid (Matrix n n α)

Matrix.specialUnitaryGroup is the group of unitary n by n matrices where the determinant is 1. (This definition is only correct if 2 is invertible.)

Defined in

Mathlib.LinearAlgebra.UnitaryGroup

Cited by

4 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintypeCommRingStarRing