Def unitarySubgroup

Modification history

2025-09-02 18:06
Mathlib/Algebra/Star/Unitary.lean
feat(Algebra/Star/Unitary): add unitarySubgroup (#11820)
Added unitarySubgroupView on Github →