mathlib

9f85080e - feat(linear_algebra/unitary_group): add a group structure on unitary_submonoid