Theorem unitarySubgroup_toSubmonoid

Modification history

2025-09-02 18:06

Mathlib/Algebra/Star/Unitary.lean

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

Added unitarySubgroup_toSubmonoid View on Github →