Commit 2024-10-09 15:32 3b8f0237

View on Github →

refactor: deprecate ContinuousMonoidHomClass (#17558) Use [ContinuousMapClass ..] [MonoidHomClass ..] instead. Also deprecate mk' since it's defeq mk.

Estimated changes

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

added structure ContinuousAddMonoidHomClass

deleted def ContinuousMonoidHom.mk'

deleted def ContinuousMonoidHom.toContinuousMap

modified structure ContinuousMonoidHom

added structure ContinuousMonoidHomClass

Modified Mathlib/Topology/Algebra/PontryaginDual.lean