mathlib

daac51e8 - feat(field_theory/adjoin): A compositum of algebraic extensions is algebraic (#15724)

feat(field_theory/adjoin): A compositum of algebraic extensions is algebraic (#15724) This PR proves that a compositum of algebraic extensions is algebraic. Coming soon to a mathlib near you: A compositum of normal extensions is normal.