[Merged by Bors] - chore(Algebra.Module.LocalizedModule): use IsLocalization instead of Localization

[xroblot]

The construction of LocalizedModule is done using IsLocalization rather than Localization. The corresponding instances for Localization are deduced automatically by Lean. One drawback is that many instances are now marked noncomputable.

---

[erdOne]

I wonder if this should be done with IsLocalizedModule?

[erdOne]

In #9210 Mathlib/RingTheory/Localization/Module.lean imports Mathlib/Algebra/Module/LocalizedModule.lean instead, which IMO is the right direction. What in that file does this PR need?

[erdOne]

Oh I see. We should probably find a better home for IsLocalizedModule.isBaseChange then.

[xroblot]

Oh I see. We should probably find a better home for IsLocalizedModule.isBaseChange then.

Yes, as you can see most of the heavy lifting is done in #9210. This PR is just about replacing Localization by IsLocalization.

[riccardobrasca]

This is strictly more general than the current situation, right?

[xroblot]

This is strictly more general than the current situation, right?

Yes, the result about Localization can be recovered since we have the instance Localization.isLocalization. In particular, Lean can automatically infer the instance about Localization from the ones about IsLocalization.

[riccardobrasca]

This is strictly more general than the current situation, right?

Yes, the result about Localization can be recovered since we have the instance Localization.isLocalization. In particular, Lean can automatically infer the instance about Localization from the ones about IsLocalization.

Thanks, let's merge this and maybe improve things later.

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded!

And happy new year! 🎉

• Build
• Check all files imported
• Lint style