mathlib3

d5146f4e - feat(ring_theory): `adjoin_root g ≃ S` if `S` has a power basis with the right minpoly (#9529)

feat(ring_theory): `adjoin_root g ≃ S` if `S` has a power basis with the right minpoly (#9529) This is basically `power_basis.equiv'` with slightly different hypotheses, specialised to `adjoin_root`. It guarantees that even over non-fields, a monogenic extension of `R` can be given by the polynomials over `R` modulo the relevant minimal polynomial.