mathlib3

327bacc4 - feat(field_theory/adjoin): `intermediate_field.to_subalgebra` distributes over supremum (#10937)

feat(field_theory/adjoin): `intermediate_field.to_subalgebra` distributes over supremum (#10937) This PR proves `(E1 ⊔ E2).to_subalgebra = E1.to_subalgebra ⊔ E2.to_subalgebra`, under the assumption that `E1` and `E2` are finite-dimensional over `F`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>