The conjugate transpose of a special unitary matrix is its adjugate #
For a special unitary matrix the conjugate transpose is the inverse, and an invertible matrix of
determinant one is its own adjugate's inverse, so the two descriptions of the inverse agree. This
turns star on Matrix.specialUnitaryGroup n α into a polynomial expression in the entries, which
is what makes the small special unitary groups computable by hand.
Main results #
Matrix.specialUnitaryGroup.star_eq_adjugate: the conjugate transpose of a special unitary matrix is its adjugate.
theorem
Matrix.specialUnitaryGroup.star_eq_adjugate
{n : Type u_1}
[Fintype n]
[DecidableEq n]
{α : Type u_2}
[CommRing α]
[StarRing α]
(g : ↥(specialUnitaryGroup n α))
:
The conjugate transpose of a special unitary matrix is its adjugate: it is the inverse, and for determinant one the inverse is the adjugate.