Def ContinuousMonoidHom.toContinuousMonoidHom

Modification history

2025-03-14 13:35

Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

feat(ContinuousMonoidHom): add notation for ContinuousMonoidHom and ContinuousAddMonoidHom (#21300) …

Modified ContinuousMonoidHom.toContinuousMonoidHom View on Github →

2025-01-22 13:36

Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

Feat(Topology/Group): add coercion toContinuousMonoidHom (#20628) …

Added ContinuousMonoidHom.toContinuousMonoidHom View on Github →