Theorem IsIntegralClosure.of_isIntegrallyClosed

Modification history

2024-05-16 14:20
Mathlib/RingTheory/IntegrallyClosed.lean
refactor: Turn Algebra.IsAlgebraic and Algebra.IsIntegral into classes (#12761) …
Deleted IsIntegralClosure.of_isIntegrallyClosedView on Github →
2023-12-19 15:21
Mathlib/RingTheory/IntegrallyClosed.lean
feat: Define the different ideal. (#9063)
Added IsIntegralClosure.of_isIntegrallyClosedView on Github →