Commit 2026-01-10 18:22 4baa4480

View on Github →

refactor: Ideal.bot_prime as an instance (#33609)

Estimated changes

Modified Mathlib/Algebra/Order/Ring/Ordering/Basic.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

Modified Mathlib/RingTheory/Ideal/GoingUp.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

Modified Mathlib/RingTheory/Ideal/Maximal.lean

Modified Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean

Modified Mathlib/RingTheory/Ideal/NatInt.lean

Modified Mathlib/RingTheory/Ideal/Prime.lean

modified theorem Ideal.bot_prime

Modified Mathlib/RingTheory/Jacobson/Ring.lean

Modified Mathlib/RingTheory/KrullDimension/Basic.lean

Modified Mathlib/RingTheory/KrullDimension/Zero.lean

Modified Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean

Modified Mathlib/RingTheory/Localization/Ideal.lean

Modified Mathlib/RingTheory/Spectrum/Prime/Basic.lean

Modified Mathlib/RingTheory/Spectrum/Prime/Topology.lean