mathlib3

e6ec9016 - feat(ring_theory/power_basis): extensionality for algebra homs (#8110)

feat(ring_theory/power_basis): extensionality for algebra homs (#8110) This PR shows two `alg_hom`s out of an algebra with a power basis are equal if the generator has the same image for both maps. It uses this result to bundle `power_basis.lift` into an equiv. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>