Theorem IsLocalization.AtPrime.liesOver_maximalIdeal

Modification history

2026-01-22 12:40
Mathlib/RingTheory/Localization/AtPrime/Basic.lean
feat(RingTheory): predicate for `QuasiFiniteAt` (#33718)
Deleted IsLocalization.AtPrime.liesOver_maximalIdealView on Github →
2025-11-12 12:36
Mathlib/RingTheory/Localization/AtPrime/Basic.lean
feat(RingTheory/Localization/AtPrime): bijection between prime ideals (#29322) …
Added IsLocalization.AtPrime.liesOver_maximalIdealView on Github →