mathlib3

8eca2934 - feat(field_theory): more general `algebra _ (algebraic_closure k)` instance (#8658)

feat(field_theory): more general `algebra _ (algebraic_closure k)` instance (#8658) For example, now we can take a field extension `L / K` and map `x : K` into the algebraic closure of `L`. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>