Commit 2021-01-16 09:11 e95988a3
View on Github →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.
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.