Commit 2021-04-14 23:14 60060c3c

feat(field_theory/algebraic_closure): define is_alg_closed.splits_codomain (#7187) Let p : polynomial K and k be an algebraically closed extension of K. Showing that p splits in k used to be a bit awkward because is_alg_closed.splits only gives splits (p.map (f : k →+* K)) id, which you still have to simp to splits p f. This PR defines is_alg_closed.splits_codomain, showing splits p f directly by doing the simping for you. It also renames polynomial.splits' to is_alg_closed.splits_domain, for symmetry. Zulip discussion starts here