Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-30 08:20 6ec7aece

View on Github →

feat(data/polynomial): ext lemmas for homomorphisms from polynomial R (#4823)

Estimated changes

Modified src/data/polynomial/algebra_map.lean

added theorem polynomial.alg_hom_ext

Modified src/data/polynomial/basic.lean

added theorem polynomial.add_hom_ext'

added theorem polynomial.add_hom_ext

added theorem polynomial.lhom_ext'

Modified src/data/polynomial/monomial.lean

added theorem polynomial.ring_hom_ext'

added theorem polynomial.ring_hom_ext