Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebra.norm_localization

Modification history

2023-02-02 10:32
src/ring_theory/localization/norm.lean
feat(ring_theory/localization): remove extraneous `algebra_map_submonoid S M ≤ S⁰` conditions (#18358)
Modified algebra.norm_localizationView on Github →
2023-01-27 17:10
src/ring_theory/localization/norm.lean
feat(ring_theory): lemmas on algebra norm (#18298) …
Added algebra.norm_localizationView on Github →