mathlib3
d35b4ff4 - chore(ring_theory): remove `splitting_field` dependency from `is_integrally_closed` (#19137)

Commit
2 years ago
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.
Author
Parents
Loading