Theorem ContinuousMonoidHom.range_toContinuousMap

Modification history

2025-02-05 09:23

Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

chore(Topology/Algebra/ContinuousMonoidHom): do not depend on `ContinuousLinearMap` (#21443) …

Modified ContinuousMonoidHom.range_toContinuousMap View on Github →

2023-12-22 06:58

Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

chore(ContinuousMonoidHom): golf (#9189)

Added ContinuousMonoidHom.range_toContinuousMap View on Github →