# Commit 2021-06-25 09:21 c5153466

View on Github →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.