Mathlib v3 is deprecated. Go to Mathlib v4

Theorem basis.localization_localization_apply

Modification history

2023-02-02 10:32
src/ring_theory/localization/module.lean
feat(ring_theory/localization): remove extraneous `algebra_map_submonoid S M ≤ S⁰` conditions (#18358)
Modified basis.localization_localization_applyView on Github →
2023-01-24 12:36
src/ring_theory/localization/module.lean
feat(ring_theory/localization): localization of a basis, again (#18261) …
Added basis.localization_localization_applyView on Github →