Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-27 20:53 0d37fd67

View on Github →

feat(data/polynomial/algebra_map): aeval_tower (#9250)

Estimated changes

Modified src/algebra/algebra/tower.lean

deleted theorem alg_hom.commutes_of_tower

added theorem alg_hom.map_algebra_map

Modified src/data/polynomial/algebra_map.lean

modified theorem polynomial.C_eq_algebra_map

added def polynomial.aeval_tower

added theorem polynomial.aeval_tower_C

added theorem polynomial.aeval_tower_X

added theorem polynomial.aeval_tower_algebra_map

added theorem polynomial.aeval_tower_comp_C

added theorem polynomial.aeval_tower_comp_algebra_map

added theorem polynomial.aeval_tower_comp_to_alg_hom

added theorem polynomial.aeval_tower_id

added theorem polynomial.aeval_tower_of_id

added theorem polynomial.aeval_tower_to_alg_hom

added theorem polynomial.alg_hom_ext'