Def LocallyConstant.toContinuousMapMonoidHom

Modification history

2023-05-10 04:45

Mathlib/Topology/ContinuousFunction/LocallyConstant.lean

feat: port Topology.ContinuousFunction.LocallyConstant (#3877)

Added LocallyConstant.toContinuousMapMonoidHom View on Github →