mathlib3

02128fe4 - feat(topology/algebra/module/character_space): add facts about `character_space.union_zero` (#16209)

feat(topology/algebra/module/character_space): add facts about `character_space.union_zero` (#16209) This adds that the `character_space` along with the zero map is a closed subspace of the `weak_dual`. The point of this is eventually to show that in the non-unital case, the `character_space` is a locally compact Hausdorff space, under appropriate assumptions.