Theorem Algebra.WeaklyQuasiFiniteAt.finite_locoalization

Modification history

2026-10-10 12:26
Mathlib/RingTheory/QuasiFinite/Weakly.lean
chore: rename `finite_locoalization` to `finite_localization` (#44643) …
Deleted Algebra.WeaklyQuasiFiniteAt.finite_locoalizationView on Github →
2026-02-13 17:17
Mathlib/RingTheory/QuasiFinite/Weakly.lean
feat(RingTheory): weakly quasi finite primes (#35234)
Added Algebra.WeaklyQuasiFiniteAt.finite_locoalizationView on Github →