Commit 2024-07-17 15:05 3ecbc035

View on Github →

chore: Split RingTheory.IntegralClosure (#14826) We create a new folder RingTheory.IntegralClosure and we move the relevant files (also doing some splitting).

Estimated changes

added theorem IsIntegral.neg
added theorem IsIntegral.of_finite
added theorem IsIntegral.smul
added def integralClosure
added theorem Algebra.isIntegral_def
added theorem IsIntegral.map
added theorem IsIntegral.of_pow
added theorem isIntegral_algHom_iff
added theorem isIntegral_algebraMap
added theorem isIntegral_one
added theorem isIntegral_zero
added def IsIntegral
deleted theorem Algebra.isIntegral_def
deleted theorem IsIntegral.map
deleted theorem IsIntegral.neg
deleted theorem IsIntegral.of_finite
deleted theorem IsIntegral.of_mem_of_fg
deleted theorem IsIntegral.of_pow
deleted theorem IsIntegral.smul
deleted def IsIntegral
deleted def RingHom.IsIntegral
deleted def integralClosure
deleted theorem isIntegral_algHom_iff
deleted theorem isIntegral_algebraMap
deleted theorem isIntegral_one
deleted theorem isIntegral_zero