Commit 2023-01-24 12:36 b69c9a77

View on Github →

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

Estimated changes

Modified src/ring_theory/localization/basic.lean

deleted theorem algebra_map_mk'

added theorem is_localization.algebra_map_apply_eq_map_map_submonoid

added theorem is_localization.algebra_map_eq_map_map_submonoid

added theorem is_localization.algebra_map_mk'

added theorem is_localization.lift_algebra_map_eq_algebra_map

added theorem is_localization.map_units_map_submonoid

Modified src/ring_theory/localization/module.lean

added theorem basis.localization_localization_apply

added theorem basis.localization_localization_repr_algebra_map

added theorem linear_independent.localization_localization

added theorem span_eq_top.localization_localization