Commit 2021-10-24 00:37 d788647fView on Github →
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.