Theorem IsLocalization.liesOver_of_isPrime_of_disjoint

Modification history

2026-01-10 16:04
Mathlib/RingTheory/Localization/AtPrime/Basic.lean
feat(RingTheory/KrullDimension): dimension of polynomial ring (#27542) …
Added IsLocalization.liesOver_of_isPrime_of_disjointView on Github →