Commit 2023-06-02 10:22 2d6ccb3e

View on Github →

feat: port RingTheory.IntegrallyClosed (#4574)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/IntegrallyClosed.lean

added theorem IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow

added theorem IsIntegrallyClosed.exists_algebraMap_eq_of_pow_mem_subalgebra

added theorem IsIntegrallyClosed.integralClosure_eq_bot

added theorem IsIntegrallyClosed.integralClosure_eq_bot_iff

added theorem IsIntegrallyClosed.isIntegral_iff

added theorem integralClosure.isIntegrallyClosedOfFiniteExtension

added theorem isIntegrallyClosed_iff

added theorem isIntegrallyClosed_iff_isIntegralClosure