Structure ContinuousAddMonoidHomClass

Modification history

2025-04-11 00:24

Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

chore: delete >6 month old deprecations (2024-10 01-10) (#23928) …

Deleted ContinuousAddMonoidHomClass View on Github →

2024-10-09 15:32

Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

refactor: deprecate `ContinuousMonoidHomClass` (#17558) …

Added ContinuousAddMonoidHomClass View on Github →