Theorem Algebra.IsIntegral.isField_iff_isField
Modification history
2025-08-09 19:57
Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
feat(RingTheory): integral extensions of comm. rings are local homs (#26746) …
Modified Algebra.IsIntegral.isField_iff_isFieldView on Github →2023-11-17 13:15
Mathlib/RingTheory/IntegralClosure.lean
chore(IntegralClosure): noncommutative generalizations and golfs (#8406) …
Modified Algebra.IsIntegral.isField_iff_isFieldView on Github →