Commit 2025-12-28 17:51 baeedfa6

chore: unify LocalizedModule and OreLocalization (#31862) We redefine LocalizedModule to be an abbrev of OreLocalization S M so that localization of a ring and localization of a module is now defeq. This is very useful to unify downstream constructions, in particular ModuleCat.tilde and Spec.structureSheaf. Some of the declarations are switched to reducible to avoid diamonds. This causes a significant performance regression, most notabaly in Mathlib/AlgebraicGeometry/AffineSpace.lean. We shall investigate if there are ways to improve performances. For example by introducing typeclasses to unify the two constructions on this and LocalizedModule, or by marking some downstream constructions (e.g. Spec.structureSheaf) as irreducible.