Theorem IsIntegralClosure.module_free

Modification history

2023-06-20 23:35

Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

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

Added IsIntegralClosure.module_free View on Github →