mathlib3

7f04253c - feat(field_theory/adjoin): Generalize alg_hom_mk_adjoin_splits to infinite sets (#5860)

feat(field_theory/adjoin): Generalize alg_hom_mk_adjoin_splits to infinite sets (#5860) This PR uses Zorn's lemma to generalize `alg_hom_mk_adjoin_splits` to infinite sets. The proof is rather long, but I think that the result is worth it. It should allow me to prove that if E/F is any normal extension then any automorphism of F lifts to an automorphism of E.