Commit 2023-06-01 16:18 d35b4ff4

chore(ring_theory): remove splitting_field dependency from is_integrally_closed (#19137) The only declarations involving splitting fields were integral_closure.mem_lifts_of_monic_of_dvd_map and is_integrally_closed.eq_map_mul_C_of_dvd. Both are similar to Gauss' lemma and their only use is to prove Gauss' lemma, so I moved them to that file.