Commit 2023-06-13 10:21 a121cf81

View on Github →

feat: port RingTheory.RingHom.Integral (#5004)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/RingHom/Integral.lean

added theorem RingHom.isIntegral_respectsIso

added theorem RingHom.isIntegral_stableUnderBaseChange

added theorem RingHom.isIntegral_stableUnderComposition