Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-18 16:15 56033982

View on Github →

feat(ring_theory/local_properties): Being finite / of finite type is local. (#10775)

Estimated changes

Modified src/ring_theory/ideal/basic.lean

added theorem ideal.span_eq_top_iff_finite

Modified src/ring_theory/ideal/operations.lean

added theorem submodule.mem_of_span_eq_top_of_smul_pow_mem

Modified src/ring_theory/local_properties.lean

added theorem finite_of_localization_span

added theorem finite_type_of_localization_span

added theorem is_localization.lift_mem_adjoin_finset_integer_multiple

added theorem is_localization.smul_mem_finset_integer_multiple_span

added theorem localization_away_map_finite

added theorem localization_away_map_finite_type

added theorem localization_finite

added theorem localization_finite_type

added theorem multiple_mem_adjoin_of_mem_localization_adjoin

added theorem multiple_mem_span_of_mem_localization_span

added theorem ring_hom.localization_away_of_localization_preserves

added def ring_hom.localization_preserves

added def ring_hom.of_localization_finite_span

added def ring_hom.of_localization_span

added theorem ring_hom.of_localization_span_iff_finite

Modified src/ring_theory/localization.lean

added def is_localization.away.map

added def localization.away_lift

added def localization.away_map