Commit 2020-09-14 16:35 a18be379

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.