The meta properties of integral ring homomorphisms.

theorem RingHom.isIntegral_stableUnderComposition : StableUnderComposition fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => f.IsIntegral

theorem RingHom.isIntegral_respectsIso : RespectsIso fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => f.IsIntegral

theorem RingHom.isIntegral_isStableUnderBaseChange : IsStableUnderBaseChange fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => f.IsIntegral

theorem RingHom.isIntegral_ofLocalizationSpan : OfLocalizationSpan fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) => x.IsIntegral

S is an integral R-algebra if there exists a set { r } that spans R such that each Sᵣ is an integral Rᵣ-algebra.