mathlib3

6bd6c11b - refactor(field_theory,ring_theory): generalize adjoin_root.equiv to `power_basis` (#8726)

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.