mathlib

ef5790b3 - feat(ring_theory/adjoin_root): golf and generalize the algebra structure on `adjoin_root`