specialUnitaryGroup and specialOrthogonalGroup

Stream: Is there code for X?

[Hunter Monroe]

specialUnitaryGroup and specialOrthogonalGroup do not exist. @Jireh Loreaux asked which of these options should be used: Matrix.unitaryGroup is just defined as a submonoid (namely the unitary submonoid). If Matrix.SpecialLinearGroup were also a submonoid (it's not defined that way), then we could just take their inf, but Matrix.SpecialLinearGroup is a hand-rolled type.

So, the question is: do we hand-roll Matrix.specialUnitaryGroup or make it the submonoid which is the inf of Matrix.unitaryGroup and the range of Matrix.SpecialLinearGroup under the coercion homomorphism?

Of course, the same applies to Matrix.specialOrthogonalGroup.

[Yaël Dillies]

See https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238774.20special.20unitary.20group

[Jireh Loreaux]

Hunter, sorry, I should have @ mentioned you when I started that thread.