Documentation

Mathlib.RingTheory.RingHom.Integral

The meta properties of integral ring homomorphisms. #

source
theorem RingHom.isIntegral_stableUnderComposition :
RingHom.StableUnderComposition fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => f.IsIntegral
source
theorem RingHom.isIntegral_respectsIso :
RingHom.RespectsIso fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => f.IsIntegral
source
theorem RingHom.isIntegral_isStableUnderBaseChange :
RingHom.IsStableUnderBaseChange fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => f.IsIntegral
source
theorem RingHom.isIntegral_ofLocalizationSpan :
RingHom.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.