mathlib3

e95988a3 - feat(field_theory/adjoin): Inductively construct algebra homomorphism (#5765)

feat(field_theory/adjoin): Inductively construct algebra homomorphism (#5765) The lemma `alg_hom_mk_adjoin_splits` can be viewed as lifting an embedding F -> K to an embedding F(S) -> K. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>