mathlib3

97ed1ee5 - feat(field_theory): more general `algebra _ (algebraic_closure k)` instance

feat(field_theory): more general `algebra _ (algebraic_closure k)` instance For example, now we can take a field extension `L / K` and map `x : K` into the algebraic closure of `L`.