Mathlib v3 is deprecated. Go to Mathlib v4

Theorem polynomial.eval_comp

Modification history

2021-03-12 04:45

src/data/polynomial/algebra_map.lean

feat(data/polynomial/*): more lemmas, especially for noncommutative rings (#6599)

Modified polynomial.eval_comp View on Github →

2020-07-16 19:13

src/data/polynomial.lean

chore(data/polynomial): break up behemoth file (#3407) …

Modified polynomial.eval_comp View on Github →

2018-11-05 05:20

data/polynomial.lean

feat(data/polynomial): polynomial.comp (#441)

Added polynomial.eval_comp View on Github →