Theorem ContinuousMonoidHom.coe_toContinuousMap

Modification history

2025-03-14 13:35
Mathlib/Topology/Algebra/ContinuousMonoidHom.lean
feat(ContinuousMonoidHom): add notation for ContinuousMonoidHom and ContinuousAddMonoidHom (#21300) …
Modified ContinuousMonoidHom.coe_toContinuousMapView on Github →
2025-01-22 13:36
Mathlib/Topology/Algebra/ContinuousMonoidHom.lean
Feat(Topology/Group): add coercion toContinuousMonoidHom (#20628) …
Added ContinuousMonoidHom.coe_toContinuousMapView on Github →