Commit 2024-12-09 18:26 e0fb3b12

View on Github →

feat(RingTheory/Ideal/Maps): generalizations from Ring to Semiring (#19715) The results generalized are about bijective ring homs. Also add lemmas comap.isMaximal and IsMaximal.comap_piEvalRingHom, which says that the preimage of a maximal ideal under the projection from a product semiring is also maximal.

Estimated changes

Modified Mathlib/RingTheory/Ideal/Maps.lean

added theorem Ideal.IsMaximal.comap_piEvalRingHom

deleted theorem Ideal.RingEquiv.bot_maximal_iff

modified theorem Ideal.comap_isMaximal_of_surjective

modified theorem Ideal.comap_le_iff_le_map

modified theorem Ideal.comap_map_of_bijective

added theorem Ideal.isMaximal_comap_iff_of_bijective

added theorem Ideal.isMaximal_iff_of_bijective

added theorem Ideal.isMaximal_map_iff_of_bijective

deleted theorem Ideal.map.isMaximal

modified def Ideal.relIsoOfBijective

Modified Mathlib/RingTheory/Jacobson/Ring.lean

Modified Mathlib/RingTheory/Nullstellensatz.lean