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.