mathlib3
0c0ab69d - feat(topology/algebra/continuous_monoid_hom): Add `topological_group` instance (#11707)

Commit
3 years ago
feat(topology/algebra/continuous_monoid_hom): Add `topological_group` instance (#11707) This PR proves that continuous monoid homs form a topological group.
Author
Parents
Loading