Commit 2023-05-10 04:45 dcf5342e

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/ContinuousFunction/LocallyConstant.lean

added def LocallyConstant.toContinuousMapAlgHom

added def LocallyConstant.toContinuousMapLinearMap

added def LocallyConstant.toContinuousMapMonoidHom