Theorem isIntegrallyClosedIn_iff

Modification history

2025-12-15 10:15

Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean

feat(Algebra): prerequisites for #31919 (#32118) …

Modified isIntegrallyClosedIn_iff View on Github →

2024-04-11 07:48

Mathlib/RingTheory/IntegrallyClosed.lean

refactor(RingTheory/IntegrallyClosed): generalize to `IsIntegrallyClosedIn` (#7857) …

Added isIntegrallyClosedIn_iff View on Github →