mathlib
b8a69951 - feat(data/polynomial): the `d-1`th coefficient of `polynomial.map` (#7639)

Commit

4 years ago

feat(data/polynomial): the `d-1`th coefficient of `polynomial.map` (#7639) We prove `polynomial.next_coeff_map` just like `polynomial.leading_coeff_map'`.

Author

Vierkantor

Parents

ccf5188f

mathlib b8a69951 - feat(data/polynomial): the `d-1`th coefficient of `polynomial.map` (#7639)

mathlib
b8a69951 - feat(data/polynomial): the `d-1`th coefficient of `polynomial.map` (#7639)