The meta properties of finite ring homomorphisms.

theorem RingHom.finite_stableUnderComposition : RingHom.StableUnderComposition @RingHom.Finite

theorem RingHom.finite_respectsIso : RingHom.RespectsIso @RingHom.Finite

theorem RingHom.finite_stableUnderBaseChange : RingHom.StableUnderBaseChange @RingHom.Finite