mathlib

ebe60290 - feat(field_theory/adjoin): Compact elements of `intermediate_field` (#15438)

feat(field_theory/adjoin): Compact elements of `intermediate_field` (#15438) This PR proves some lemmas regarding compact elements of `intermediate_field`, essentially copying the analogous results for `submodule` from `linear_algebra/span.lean`. This PR combos with #15419. Co-authored-by: tb65536 <tb65536@users.noreply.github.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>