mathlib

7310eab9 - feat(field_theory/adjoin): adjoining elements to fields (#3913)

feat(field_theory/adjoin): adjoining elements to fields (#3913) Defines adjoining elements to fields Co-authored-by: tb65536 <tb65536@users.noreply.github.com> Co-authored-by: Patrick Lutz <pglutz@berkeley.edu>