Commit 2023-03-03 19:32 3d494381

View on Github →

feat: port Topology.LocallyConstant.Algebra (#2592)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/LocallyConstant/Algebra.lean

added theorem LocallyConstant.charFn_eq_one

added theorem LocallyConstant.charFn_eq_zero

added theorem LocallyConstant.charFn_inj

added def LocallyConstant.coeFnMonoidHom

added theorem LocallyConstant.coe_algebraMap

added theorem LocallyConstant.coe_charFn

added theorem LocallyConstant.coe_div

added theorem LocallyConstant.coe_inv

added theorem LocallyConstant.coe_mul

added theorem LocallyConstant.coe_one

added theorem LocallyConstant.coe_smul

added def LocallyConstant.constMonoidHom

added def LocallyConstant.constRingHom

added theorem LocallyConstant.div_apply

added theorem LocallyConstant.inv_apply

added theorem LocallyConstant.mul_apply

added theorem LocallyConstant.one_apply

added theorem LocallyConstant.smul_apply