Def unitarySubgroupUnitsEquiv

Modification history

2025-09-02 18:06

Mathlib/Algebra/Star/Unitary.lean

feat(Algebra/Star/Unitary): add unitarySubgroup (#11820)

Added unitarySubgroupUnitsEquiv View on Github →