Theorem mem_unitarySubgroup_iff

Modification history

2025-09-02 18:06

Mathlib/Algebra/Star/Unitary.lean

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

Added mem_unitarySubgroup_iff View on Github →