Commit 2021-10-08 10:04 d5146f4e

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.