Commit 2021-10-24 00:37 d788647f

View on Github →

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.

Estimated changes