Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-27 11:14 01c60b26

View on Github →

feat(ring_theory/ring_hom/finite): Finite type is a local property (#15379)

Estimated changes

Modified src/algebra/algebra/subalgebra/basic.lean

added theorem subalgebra.mem_of_span_eq_top_of_smul_pow_mem

Modified src/ring_theory/adjoin/basic.lean

added theorem algebra.pow_smul_mem_of_smul_subset_of_mem_adjoin

Modified src/ring_theory/local_properties.lean

added theorem is_localization.exists_smul_mem_of_mem_adjoin

added def ring_hom.of_localization_finite_span_target

added theorem ring_hom.of_localization_span_target_iff_finite

Created src/ring_theory/ring_hom/finite_type.lean

added theorem ring_hom.finite_is_local

added theorem ring_hom.finite_type_holds_for_localization_away

added theorem ring_hom.finite_type_of_localization_span_target

added theorem ring_hom.finite_type_stable_under_composition