Commit 2023-08-18 21:51 efc5aeb0

View on Github →

feat: algebraic maps in LocallyConstant (#6520) We define more algebraic versions of LocallyConstant.comap and evaluation of locally constant maps, continuing the work of #6396.

Estimated changes

Modified Mathlib/Topology/LocallyConstant/Algebra.lean

added def LocallyConstant.coeFnAlgHom

added def LocallyConstant.coeFnRingHom

added def LocallyConstant.coeFnₗ

added def LocallyConstant.comapMulHom

added def LocallyConstant.comapRingHom

added def LocallyConstant.comapₐ

modified def LocallyConstant.comapₗ

added def LocallyConstant.congrLeftMulEquiv

added def LocallyConstant.congrLeftRingEquiv

added def LocallyConstant.congrLeftₐ

modified def LocallyConstant.congrLeftₗ

added def LocallyConstant.evalMonoidHom

added def LocallyConstant.evalRingHom

added def LocallyConstant.evalₐ

added def LocallyConstant.evalₗ

modified theorem LocallyConstant.ker_comapₗ

Modified Mathlib/Topology/LocallyConstant/Basic.lean