mathlib3

b69c9a77 - feat(ring_theory/localization): localization of a basis, again (#18261)

feat(ring_theory/localization): localization of a basis, again (#18261) This PR replaces `basis.localization` with `basis.localization_localization`, which maps `basis ι R S` to `basis ι Rm Sm`, where `Rm` and `Sm` are the localizations of `R` and `S` at `m`. This differs from the existing `basis.localization` by localizing in two places at once, since localizing only the coefficients is probably not useful. See also: #18150 Co-authored-by: Vierkantor <vierkantor@vierkantor.com>