mathlib

c5153466 - feat(ring_theory/power_basis): map a power basis through an alg_equiv (#8039)

feat(ring_theory/power_basis): map a power basis through an alg_equiv (#8039) If `A` is equivalent to `A'` as an `R`-algebra and `A` has a power basis, then `A'` also has a power basis. Included are the relevant `simp` lemmas. This needs a bit of tweaking to `basis.map` and `alg_equiv.to_linear_equiv` for getting more useful `simp` lemmas.