Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-12 10:06 912c47d3

View on Github →

feat(topology/algebra/continuous_monoid_hom): New file (#11304) This PR defines continuous monoid homs.

Estimated changes

Created src/topology/algebra/continuous_monoid_hom.lean

added structure continuous_add_monoid_hom

added def continuous_monoid_hom.comp

added def continuous_monoid_hom.coprod

added def continuous_monoid_hom.diag

added theorem continuous_monoid_hom.ext

added def continuous_monoid_hom.fst

added def continuous_monoid_hom.id

added def continuous_monoid_hom.inl

added def continuous_monoid_hom.inr

added def continuous_monoid_hom.inv

added def continuous_monoid_hom.mk'

added def continuous_monoid_hom.mul

added def continuous_monoid_hom.one

added def continuous_monoid_hom.prod

added def continuous_monoid_hom.prod_map

added def continuous_monoid_hom.snd

added def continuous_monoid_hom.swap

added structure continuous_monoid_hom