Theorem IsIntegrallyClosedIn.isIntegral_iff

Modification history

2024-08-09 00:58

Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean

chore: backports for leanprover/lean4#4814 (part 24) (#15520)

Modified IsIntegrallyClosedIn.isIntegral_iff View on Github →

2024-04-11 07:48

Mathlib/RingTheory/IntegrallyClosed.lean

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

Added IsIntegrallyClosedIn.isIntegral_iff View on Github →