ring_theory.ring_hom.finite_type
source
The main result is ring_hom.finite_is_local.
ring_hom.finite_is_local