Commit 2021-06-25 09:21 c5153466

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.