Commit 2021-08-18 10:32 6bd6c11b

refactor(field_theory,ring_theory): generalize adjoin_root.equiv to power_basis (#8726) We had two proofs that A-preserving maps from A[x] or A(x) to B are in bijection with the set of conjugate roots to x in B, so by stating the result for power_basis we can avoid reproving it twice, and get some generalizations (to a comm_ring instead of an integral_domain) for free. There's probably a bit more to generalize in adjoin_root or intermediate_field.adjoin, which I will do in follow-up PRs.