Theorem isIntegrallyClosed_iff_isIntegralClosure

Modification history

2023-06-02 10:22
Mathlib/RingTheory/IntegrallyClosed.lean
feat: port RingTheory.IntegrallyClosed (#4574)
Added isIntegrallyClosed_iff_isIntegralClosureView on Github →