Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-04 01:49 2dd78b8d

View on Github →

feat(data/polynomial): add eval2 for univariate polys

Estimated changes

Modified algebra/group_power.lean

modified theorem int.coe_nat_pow

added theorem is_semiring_hom.map_pow

Modified data/polynomial.lean

modified def polynomial.eval

modified theorem polynomial.eval_C

modified theorem polynomial.eval_X

modified theorem polynomial.eval_add

modified theorem polynomial.eval_mul

modified theorem polynomial.eval_one

modified theorem polynomial.eval_pow

modified theorem polynomial.eval_zero

added def polynomial.eval₂

added theorem polynomial.eval₂_C

added theorem polynomial.eval₂_X

added theorem polynomial.eval₂_add

added theorem polynomial.eval₂_mul

added theorem polynomial.eval₂_one

added theorem polynomial.eval₂_pow

added theorem polynomial.eval₂_zero

added def polynomial.map

added theorem polynomial.map_C

added theorem polynomial.map_X

added theorem polynomial.map_add

added theorem polynomial.map_mul

added theorem polynomial.map_one

added theorem polynomial.map_pow

added theorem polynomial.map_zero

Modified linear_algebra/multivariate_polynomial.lean