Commit 2023-08-11 23:48 ec529253

feat: add Algebra.discr_localizationLocalization (#6422) We prove

theorem Algebra.discr_localizationLocalization (b : Basis ι R S) :
  Algebra.discr Rₘ (b.localizationLocalization Rₘ M Aₘ) = algebraMap R Rₘ (Algebra.discr R b) 

We need for that to prove the analogue for the trace of Algebra.norm_localization (that was the only result in RingTheory.Localization.Norm). Since the results are added to this file, it is renamed to RingTheory.Localization.NormTrace (not sure about the name though).