Mathlib Map

Theorems · Definition · group theory

Matrix.unitaryGroup

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

Matrix.unitaryGroup n is the group of n by n matrices where the star-transpose is the inverse.

Defined in
Mathlib.LinearAlgebra.UnitaryGroup
Cited by
37 results in Mathlib
Foundations
Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
DecidableEqFintypeCommRingStarRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Matrix.IsHermitian.eigenvectorUnitary · cited by 25IsHermitian.eigenvectorUn…Matrix.orthogonalGroup · cited by 4Matrix.orthogonalGroupMatrix.det_of_mem_unitary · cited by 4Matrix.det_of_mem_unitaryMatrix.specialUnitaryGroup · cited by 4Matrix.specialUnitaryGroupMatrix.UnitaryGroup.toLin' · cited by 4UnitaryGroup.toLin'Matrix.mem_unitaryGroup_iff · cited by 3Matrix.mem_unitaryGroup_i…Matrix.mem_unitaryGroup_iff' · cited by 3Matrix.mem_unitaryGroup_i…OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary · cited by 3OrthonormalBasis.toMatrix…Matrix.UnitaryGroup.map_star · cited by 3UnitaryGroup.map_starMatrix.UnitaryGroup.toGL · cited by 3UnitaryGroup.toGLMatrix.UnitaryGroup.transpose · cited by 3UnitaryGroup.transposeMatrix.IsHermitian.eigenvectorUnitary_mulVec · cited by 2IsHermitian.eigenvectorUn…LinearIsometryEquiv.toMatrix_mem_unitaryGroup · cited by 1LinearIsometryEquiv.toMat…Matrix.IsHermitian.star_eigenvectorUnitary_mulVec · cited by 1IsHermitian.star_eigenvec…Matrix.UnitaryGroup.toLin'_one · cited by 1UnitaryGroup.toLin'_oneCommRing · cited by 17173CommRingFintype · cited by 7736FintypeMatrix · cited by 4303MatrixSubmonoid · cited by 3086SubmonoidStarRing · cited by 1686StarRingunitary · cited by 207unitaryMatrix.unitaryGroupCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • CommRingstatement and proof · cited by 17,173
  • Fintypestatement and proof · cited by 7,736
  • Matrixstatement and proof · cited by 4,303
  • Submonoidstatement · cited by 3,086
  • StarRingstatement and proof · cited by 1,686
  • unitaryproof · cited by 207

Cited by46

Results whose statement or proof uses this declaration.