mathlib3

1362701b - refactor(field_theory): Adjoin intermediate field (#4468)

refactor(field_theory): Adjoin intermediate field (#4468) Refactor adjoin to be an intermediate field rather than a subalgebra. Co-authored-by: Patrick Lutz <pglutz@berkeley.edu>