Theorem Algebra.norm_localization

Modification history

2023-08-11 23:48
Mathlib/RingTheory/Localization/Norm.lean
feat: add Algebra.discr_localizationLocalization (#6422) …
Modified Algebra.norm_localizationView on Github →
2023-06-20 16:28
Mathlib/RingTheory/Localization/Norm.lean
feat: port RingTheory.Localization.Norm (#5299)
Added Algebra.norm_localizationView on Github →