Def Ideal.primeCompl

Modification history

2025-02-07 16:33

Mathlib/RingTheory/Ideal/Prime.lean

chore(RingTheory/Ideal/Over): factor going-up results out (#21497) …

Modified Ideal.primeCompl View on Github →

2023-05-19 11:12

Mathlib/RingTheory/Localization/AtPrime.lean

feat: port RingTheory.Localization.AtPrime (#4086)

Added Ideal.primeCompl View on Github →