mathlib documentation

ring_theory.ring_hom.finite

The meta properties of finite ring homomorphisms. #

source
theorem ring_hom.finite_stable_under_composition  :
ring_hom.stable_under_composition ring_hom.finite
source
theorem ring_hom.finite_respects_iso  :
ring_hom.respects_iso ring_hom.finite
source
theorem ring_hom.finite_stable_under_base_change  :
ring_hom.stable_under_base_change ring_hom.finite