mathlib

7f034c52 - feat(topology/algebra/module/character_space): kernels of terms of the `character_space` (#16722)

feat(topology/algebra/module/character_space): kernels of terms of the `character_space` (#16722) This shows that the kernel of a element `φ` of `character_space 𝕜 A` is a maximal ideal. Moreover, `φ` and `ψ` are equal if their kernels coincide. In addition, we provide a missing `ext` lemma, and protect a lemma named `is_closed` in this namespace.