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_stableUnderBaseChange :
RingHom.StableUnderBaseChange fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => f.IsIntegral