Theorem LocallyConstant.toLinearMap_toContinuousMapAlgHom

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.toLinearMap_toContinuousMapAlgHomView on Github →