mathlib3

c596622f - feat(field_theory/intermediate_field): Inhabited instance (#18956)

feat(field_theory/intermediate_field): Inhabited instance (#18956) If `S : intermediate_field K L`, then `S →ₐ[K] L` is nonempty. Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>