Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-18 10:32 6bd6c11b

View on Github →

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.

Estimated changes