Theorem isClosed_unitary

Modification history

2025-11-04 18:11
Mathlib/Topology/Algebra/Star/Unitary.lean
feat(Topology/Algebra/Star): the unitary group in a T1 monoid is closed (#31136)
Added isClosed_unitaryView on Github →