Commit 2024-06-07 11:26 1df6b982

View on Github →

feat(Topology/LocallyConstant): map and const as algebraic maps (#12508) This PR adds algebraic versions of LocallyConstant.map and LocallyConstant.const given various algebraic structures on the target. Follows the existing approach for LocallyConstant.comap.

Estimated changes

Modified Mathlib/Topology/LocallyConstant/Algebra.lean

deleted def LocallyConstant.comapMulHom

deleted def LocallyConstant.congrLeftMulEquiv

added def LocallyConstant.congrRightRingEquiv

added def LocallyConstant.congrRightₐ

added def LocallyConstant.congrRightₗ

added def LocallyConstant.constₐ

added def LocallyConstant.constₗ

added def LocallyConstant.mapMonoidHom

added def LocallyConstant.mapRingHom

added def LocallyConstant.mapₐ

added def LocallyConstant.mapₗ

Modified Mathlib/Topology/LocallyConstant/Basic.lean

added def LocallyConstant.congrRight

added def LocallyConstant.piecewise'