Theorem Localization.finite_of_primesOver_eq_singleton

Modification history

2026-09-03 08:22
Mathlib/RingTheory/Unramified/LocalRing.lean
refactor(RingTheory/Localization/AtPrime/Basic): replace `IsLiesOverAlgebra` with `IsScalarTower` (#41100) …
Modified Localization.finite_of_primesOver_eq_singletonView on Github →
2026-05-01 19:07
Mathlib/RingTheory/Unramified/LocalRing.lean
refactor(Localization/AtPrime/Basic): add predicate for algebra instance on `Localization.AtPrime` (#38465) …
Modified Localization.finite_of_primesOver_eq_singletonView on Github →
2026-02-09 11:07
Mathlib/RingTheory/Unramified/LocalRing.lean
feat(RingTheory): local structure for finite unramified algebras (#34928)
Added Localization.finite_of_primesOver_eq_singletonView on Github →