mathlib3

050b8370 - feat(field_theory/adjoin): Adjoin integral element (#4831)

feat(field_theory/adjoin): Adjoin integral element (#4831) Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: tb65536 <tb65536@users.noreply.github.com>