Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes