Theorem exists_integral_multiples

Modification history

2023-06-20 23:35

Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

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

Added exists_integral_multiples View on Github →