mathlib3

d788647f - feat(ring_theory): generalize `adjoin_root.power_basis` (#9536)

feat(ring_theory): generalize `adjoin_root.power_basis` (#9536) Now we only need that `g` is monic to state that `adjoin_root g` has a power basis. Note that this does not quite imply the result of #9529: this is phrased in terms of `minpoly R (root g)` and the other PR in terms of `g` itself, so I don't have a direct use for the current PR. However, it seems useful enough to have this statement, so I PR'd it anyway. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>