mathlib3

0081a5a4 - feat(ring_theory/algebraic): if `L / K` is algebraic, then the subalgebras are fields (#4903)