Theorem IsTopologicalTorsor.to_isTopologicalGroup

Modification history

2026-06-12 09:16
Mathlib/Topology/Algebra/Group/AddTorsor.lean
feat(Topology/Algebra): topological multiplicative torsors (#39130) …
Added IsTopologicalTorsor.to_isTopologicalGroupView on Github →