Mathlib.RingTheory.RingHom.FiniteType
source
The main result is RingHom.finiteType_is_local.
RingHom.finiteType_is_local