mathlib3

a18be379 - feat(ring_theory/ideal/over): Going up theorem for integral extensions (#4064)

feat(ring_theory/ideal/over): Going up theorem for integral extensions (#4064) The main statement is `exists_ideal_over_prime_of_is_integral` which shows that for an integral extension, every prime ideal of the original ring lies under some prime ideal of the extension ring. `is_field_of_is_integral_of_is_field` is a brute force proof that if `R → S` is an integral extension, and `S` is a field, then `R` is also a field (using the somewhat new `is_field` proposition). `is_maximal_comap_of_is_integral_of_is_maximal` Gives essentially the same statement in terms of maximal ideals. `disjoint_compl` has also been replaced with `disjoint_compl_left` and `disjoint_compl_right` variants. Co-authored-by: Devon Tuma <dtumad@gmail.com>