Theorem LocallyConstant.toAddMonoidHom_toContinuousMapLinearMap

Modification history

2026-02-17 17:59

Mathlib/Topology/ContinuousMap/LocallyConstant.lean

feat(Topology/ContinuousMap/LocallyConstant): the range of `toContinuousMapAlgHom` separates points (#35221) …

Added LocallyConstant.toAddMonoidHom_toContinuousMapLinearMap View on Github →