Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-13 09:46 e26b459d

View on Github →

feat(data/polynomial): some lemmas about eval2 and algebra_map (#3382)

Estimated changes

Modified src/data/polynomial.lean

added theorem polynomial.C_eq_algebra_map

added theorem polynomial.alg_hom_eval₂_algebra_map

added theorem polynomial.eval₂_algebra_map_X

added theorem polynomial.eval₂_algebra_map_int_X

added theorem polynomial.ring_hom_eval₂_algebra_map_int

Modified src/ring_theory/algebra.lean

added theorem algebra.algebra_ext

added def ring_hom.to_int_alg_hom