Commit 2021-10-08 10:04 82e2b98a

feat(ring_theory): generalize power_basis.equiv (#9528) power_basis.equiv' is an alternate formulation of power_basis.equiv that is somewhat more general when not over a field: instead of requiring the minimal polynomials are equal, we only require the generators are the roots of each other's minimal polynomials. This is not quite enough to show adjoin_root (minpoly R (pb : power_basis R S).gen) is isomorphic to S, since minpoly R (adjoin_root.root g) is not guaranteed to have the same exact roots as g itself. So in a follow-up PR I will strengthen power_basis.equiv' to adjoin_root.equiv' that requires the correct hypothesis.