Theorem IsIntegralClosure.module_free

Modification history

2026-01-13 19:40
Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …
Modified IsIntegralClosure.module_freeView on Github →
2023-06-20 23:35
Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean
feat: port RingTheory.DedekindDomain.IntegralClosure (#5304)
Added IsIntegralClosure.module_freeView on Github →