Commit 2025-01-22 13:36 fe4e3aba

View on Github →

Feat(Topology/Group): add coercion toContinuousMonoidHom (#20628) Add coercion toContinuousMonoidHom when [MonoidHomClass F A B] [ContinuousMapClass F A B]

Estimated changes

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

added theorem ContinuousMonoidHom.coe_coe

added theorem ContinuousMonoidHom.coe_toContinuousMap

added theorem ContinuousMonoidHom.coe_toMonoidHom

added theorem ContinuousMonoidHom.toContinuousMap_toContinuousMonoidHom

added def ContinuousMonoidHom.toContinuousMonoidHom

added theorem ContinuousMonoidHom.toMonoidHom_toContinuousMonoidHom