mathlib

bff41725 - feat(field_theory/adjoin): The compositum of finitely many finite dimensional intermediate fields is finite dimensional, finset version (#15426)

feat(field_theory/adjoin): The compositum of finitely many finite dimensional intermediate fields is finite dimensional, finset version (#15426) This PR adds a finset version of `finite_dimensional_supr_of_finite`, since `⨆ i ∈ s` seems to be the best way to talk about finite compositums in practice.