Commit 2022-07-15 07:02 daf11179

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.