mathlib

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

feat(field_theory/algebraic_closure): map from algebraic extensions into the algebraic closure (#9110) Co-authored-by: Chris Hughes <chrishughes24@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: kckennylau <kc_kennylau@yahoo.com.hk>