Commit 2025-03-14 13:35 c529790e

View on Github →

feat(ContinuousMonoidHom): add notation for ContinuousMonoidHom and ContinuousAddMonoidHom (#21300) This PR adds notation for ContinuousMonoidHom and ContinuousAddMonoidHom.

Estimated changes

Modified Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean

modified theorem ProfiniteGrp.hom_ofHom

modified theorem ProfiniteGrp.ofHom_apply

modified theorem ProfiniteGrp.ofHom_comp

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

modified theorem ContinuousMonoidHom.coe_one

modified theorem ContinuousMonoidHom.coe_toContinuousMap

modified theorem ContinuousMonoidHom.coe_toMonoidHom

modified def ContinuousMonoidHom.comp

modified def ContinuousMonoidHom.diag

modified theorem ContinuousMonoidHom.ext

modified def ContinuousMonoidHom.fst

modified def ContinuousMonoidHom.id

modified def ContinuousMonoidHom.inl

modified def ContinuousMonoidHom.inr

modified def ContinuousMonoidHom.mul

modified def ContinuousMonoidHom.prod

modified def ContinuousMonoidHom.prodMap

modified def ContinuousMonoidHom.snd

modified def ContinuousMonoidHom.swap

modified def ContinuousMonoidHom.toContinuousMonoidHom

Modified Mathlib/Topology/Algebra/PontryaginDual.lean

modified theorem PontryaginDual.map_apply

modified theorem PontryaginDual.map_comp

modified theorem PontryaginDual.map_one