mathlib

8062521e - feat(topology/locally_constant): Adding a module structure to locally constant functions (#8384)

feat(topology/locally_constant): Adding a module structure to locally constant functions (#8384) We add an A-module structure to locally constant functions from a topological space to a semiring A. This also adds the lemmas `coe_zero`, `coe_add`, `coe_neg`, `coe_sub`, `coe_one`, `coe_mul`, `coe_div`, `coe_inv` to match the new `coe_smul` lemma. Co-authored-by: laughinggas <58670661+laughinggas@users.noreply.github.com> Co-authored-by: Oliver Nash <github@olivernash.org>