Commit 2023-06-20 23:35 e7f7075f

View on Github →

feat: port RingTheory.DedekindDomain.IntegralClosure (#5304)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

added theorem FiniteDimensional.exists_is_basis_integral

added theorem IsIntegralClosure.isDedekindDomain

added theorem IsIntegralClosure.isLocalization

added theorem IsIntegralClosure.isNoetherian

added theorem IsIntegralClosure.isNoetherianRing

added theorem IsIntegralClosure.module_free

added theorem IsIntegralClosure.range_le_span_dualBasis

added theorem IsIntegralClosure.rank

added theorem exists_integral_multiples

added theorem integralClosure.isDedekindDomain

added theorem integralClosure.isNoetherianRing

added theorem integralClosure_le_span_dualBasis