Theorem integralClosure.isIntegrallyClosedOfFiniteExtension

Modification history

2023-09-14 10:14
Mathlib/RingTheory/IntegrallyClosed.lean
refactor: remove `IsDomain` hypothesis from `IsIntegrallyClosed` (#6126) …
Modified integralClosure.isIntegrallyClosedOfFiniteExtensionView on Github →
2023-06-02 10:22
Mathlib/RingTheory/IntegrallyClosed.lean
feat: port RingTheory.IntegrallyClosed (#4574)
Added integralClosure.isIntegrallyClosedOfFiniteExtensionView on Github →