The meta properties of finite-type ring homomorphisms.

The main result is RingHom.finiteType_is_local.

theorem RingHom.finiteType_stableUnderComposition : RingHom.StableUnderComposition @RingHom.FiniteType

theorem RingHom.finiteType_holdsForLocalizationAway : RingHom.HoldsForLocalizationAway @RingHom.FiniteType

theorem RingHom.finiteType_ofLocalizationSpanTarget : RingHom.OfLocalizationSpanTarget @RingHom.FiniteType

theorem RingHom.finiteType_is_local : RingHom.PropertyIsLocal @RingHom.FiniteType

theorem RingHom.finiteType_respectsIso : RingHom.RespectsIso @RingHom.FiniteType