Theorem ContinuousMonoidHom.coe_toMonoidHom

Modification history

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