Commit 2021-07-23 11:58 8062521e

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.