mathlib3

73421d52 - feat(field_theory/adjoin): `intermediate_field.adjoin` equals `subalgebra.adjoin` for algebraic sets (#15762)

feat(field_theory/adjoin): `intermediate_field.adjoin` equals `subalgebra.adjoin` for algebraic sets (#15762) This PR proves `(intermediate_field.adjoin F S).to_subalgebra = algebra.adjoin F S` for algebraic sets `S`.