Commit 2022-01-31 09:46 0c0ab69d

View on Github →

feat(topology/algebra/continuous_monoid_hom): Add topological_group instance (#11707) This PR proves that continuous monoid homs form a topological group.

Estimated changes

Modified src/topology/algebra/continuous_monoid_hom.lean

added theorem continuous_monoid_hom.is_embedding

added theorem continuous_monoid_hom.is_inducing