Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-02 10:32 2e59a6de

View on Github →

feat(ring_theory/localization): remove extraneous algebra_map_submonoid S M ≤ S⁰ conditions (#18358)

Estimated changes

Modified src/ring_theory/ideal/norm.lean

Modified src/ring_theory/localization/module.lean

modified theorem basis.localization_localization_apply

modified theorem basis.localization_localization_repr_algebra_map

modified theorem linear_independent.localization_localization

Modified src/ring_theory/localization/norm.lean

modified theorem algebra.norm_localization