Commit 2021-06-29 20:21 e6ec9016

View on Github →

feat(ring_theory/power_basis): extensionality for algebra homs (#8110) This PR shows two alg_homs 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.

Estimated changes

Modified src/algebra/algebra/basic.lean

added theorem alg_hom.subsingleton

Modified src/ring_theory/power_basis.lean

added theorem power_basis.alg_hom_ext

modified theorem power_basis.constr_pow_mul

modified theorem power_basis.equiv_aeval

modified theorem power_basis.equiv_gen

modified theorem power_basis.equiv_map

modified theorem power_basis.equiv_symm

added theorem power_basis.exists_eq_aeval'

modified theorem power_basis.lift_aeval

modified theorem power_basis.lift_gen