mathlib

5c05ca28 - feat(ring_theory/integral_closure): `is_field_iff_is_field` (#10875)

feat(ring_theory/integral_closure): `is_field_iff_is_field` (#10875) If `R/S` is an integral extension, then `R` is a field if and only if `S` is a field. One direction was already in mathlib, and this PR proves the converse direction.