Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-14 05:43 073c3ace

View on Github →

feat(ring_theory): Basic framework for classes of ring homomorphisms (#14966)

Estimated changes

Modified src/ring_theory/local_properties.lean

added theorem localization_preserves_surjective

added def ring_hom.holds_for_localization_away

deleted theorem ring_hom.localization_away_of_localization_preserves

added theorem ring_hom.localization_preserves.away

added def ring_hom.of_localization_prime

added def ring_hom.of_localization_span_target

added theorem ring_hom.property_is_local.of_localization_span

added theorem ring_hom.property_is_local.respects_iso

added structure ring_hom.property_is_local

added theorem surjective_of_localization_span

Modified src/ring_theory/localization/away.lean

added theorem is_localization.away_of_is_unit_of_bijective

Created src/ring_theory/ring_hom_properties.lean

added theorem ring_hom.respects_iso.cancel_left_is_iso

added theorem ring_hom.respects_iso.cancel_right_is_iso

added theorem ring_hom.respects_iso.is_localization_away_iff

added def ring_hom.respects_iso

added theorem ring_hom.stable_under_base_change.pushout_inl

added def ring_hom.stable_under_base_change

added theorem ring_hom.stable_under_composition.respects_iso

added def ring_hom.stable_under_composition