Commit 2023-08-10 11:44 461da4ad

View on Github →

feat: algebraic versions of LocallyConstant.comap (#6396) We give algebraic versions of LocallyConstant.comap given the relevant algebraic structure on the target.

Estimated changes

Modified Mathlib/Topology/LocallyConstant/Algebra.lean

added def LocallyConstant.comapMonoidHom

added def LocallyConstant.comapₗ

added def LocallyConstant.congrLeftₗ

added theorem LocallyConstant.ker_comapₗ

Modified Mathlib/Topology/LocallyConstant/Basic.lean

added theorem LocallyConstant.coe_comap_apply

added theorem LocallyConstant.comap_comap

modified theorem LocallyConstant.comap_id

added theorem LocallyConstant.comap_injective

added def LocallyConstant.congrLeft