mathlib3 documentation

ring_theory.ring_hom.finite

The meta properties of finite ring homomorphisms. #

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

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