Commit 2023-12-31 14:56 a59d0136
View on Github →chore(Algebra.Module.LocalizedModule): use IsLocalization instead of Localization (#9167)
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.