Commit 2025-09-02 18:06 9c51141d

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Star/Unitary.lean

added theorem mem_unitarySubgroup_iff

added theorem unitary.inv_mem

added def unitarySubgroup

added def unitarySubgroupUnitsEquiv

added theorem unitarySubgroup_toSubmonoid