mathlib3

daf11179 - feat(field_theory/tower): if `L / K / F` is finite, so is `K / F` (#15303)

feat(field_theory/tower): if `L / K / F` is finite, so is `K / F` (#15303) This result came up in the discussion of #15191, where I couldn't find it. (In the end we didn't up needing it.) I saw we already had finiteness of `L / K` (in fact, for any vector space instead of the field `L`) as `finite_dimensional.right`, so I made the `left` version too. Also use this to provide an instance where `K` is an intermediate field. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>