mathlib3 documentation

ring_theory.ring_hom.finite_type

The meta properties of finite-type ring homomorphisms. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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