mathlib documentation

ring_theory.ring_hom.finite_type

The meta properties of finite-type ring homomorphisms. #

The main result is ring_hom.finite_is_local.

source
theorem ring_hom.finite_type_stable_under_composition  :
ring_hom.stable_under_composition ring_hom.finite_type
source
theorem ring_hom.finite_type_holds_for_localization_away  :
ring_hom.holds_for_localization_away ring_hom.finite_type
source
theorem ring_hom.finite_type_of_localization_span_target  :
ring_hom.of_localization_span_target ring_hom.finite_type
source
theorem ring_hom.finite_type_is_local  :
ring_hom.property_is_local ring_hom.finite_type
source
theorem ring_hom.finite_type_respects_iso  :
ring_hom.respects_iso ring_hom.finite_type