mathlib3

57c7d940 - feat(field_theory/adjoin): The compositum of finitely many finite dimensional intermediate fields is finite dimensional (#15339)

feat(field_theory/adjoin): The compositum of finitely many finite dimensional intermediate fields is finite dimensional (#15339) This PR adds an instance stating that the compositum of finitely many finite dimensional intermediate fields is finite dimensional. The proof is a bit janky, unfortunately. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>