mathlib

70ca6fd8 - feat(ring_theory/power_basis): `equiv`s between algebras with the same power basis (#4986)

feat(ring_theory/power_basis): `equiv`s between algebras with the same power basis (#4986) `power_basis.lift` and `power_basis.equiv` use the power basis structure to define `alg_hom`s and `alg_equiv`s. The main application in this PR is `power_basis.equiv_adjoin_simple`, which states that adjoining an element of a power basis of `L : K` gives `L` itself.