Commit 2026-10-10 12:26 a960fdae

View on Github →

chore: rename finite_locoalization to finite_localization (#44643) Fixes the misspelling locoalization in WeaklyQuasiFiniteAt.finite_locoalization. 🤖 Generated with Claude Code

Estimated changes

Modified Mathlib/RingTheory/QuasiFinite/Polynomial.lean

Modified Mathlib/RingTheory/QuasiFinite/Weakly.lean

added theorem Algebra.WeaklyQuasiFiniteAt.finite_localization

deleted theorem Algebra.WeaklyQuasiFiniteAt.finite_locoalization