Def lift.subfield_with_hom.maximal_subfield_with_hom

refactor(field_theory/algebraic_closure): Move construction of algebraic closure and lemmas about alg closed fields into seperate files. (#9265)

feat(field_theory/algebraic_closure): map from algebraic extensions into the algebraic closure (#9110)