Commit 2022-10-01 15:41 7f034c52
View on Github →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.