Commit 2023-05-22 16:36 b6c41003

View on Github →

feat: port RingTheory.IntegralClosure (#4196) I tried to fix what I could, but this contains a lot of sorries!

Estimated changes

added theorem FG_adjoin_of_finite
added theorem IsIntegral.algebraMap
added theorem IsIntegral.det
added theorem IsIntegral.nsmul
added theorem IsIntegral.pow
added theorem IsIntegral.pow_iff
added theorem IsIntegral.prod
added theorem IsIntegral.sum
added theorem IsIntegral.tmul
added theorem IsIntegral.zsmul
added def IsIntegral
added theorem Module.End.isIntegral
added def integralClosure
added theorem integralClosure_idem
added theorem isIntegral_add
added theorem isIntegral_algEquiv
added theorem isIntegral_algHom_iff
added theorem isIntegral_algebraMap
added theorem isIntegral_mul
added theorem isIntegral_neg
added theorem isIntegral_ofSubring
added theorem isIntegral_of_pow
added theorem isIntegral_one
added theorem isIntegral_smul
added theorem isIntegral_sub
added theorem isIntegral_sup
added theorem isIntegral_trans
added theorem isIntegral_trans_aux
added theorem isIntegral_zero
added theorem map_isIntegral
added theorem map_isIntegral_int