Commit 2023-06-05 10:31 fb8ee975

View on Github →

feat: port RingTheory.Polynomial.Bernstein (#4661)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Polynomial/Bernstein.lean

added theorem bernsteinPolynomial.derivative_succ

added theorem bernsteinPolynomial.derivative_succ_aux

added theorem bernsteinPolynomial.derivative_zero

added theorem bernsteinPolynomial.eq_zero_of_lt

added theorem bernsteinPolynomial.eval_at_0

added theorem bernsteinPolynomial.eval_at_1

added theorem bernsteinPolynomial.flip'

added theorem bernsteinPolynomial.flip

added theorem bernsteinPolynomial.iterate_derivative_at_0

added theorem bernsteinPolynomial.iterate_derivative_at_0_eq_zero_of_lt

added theorem bernsteinPolynomial.iterate_derivative_at_0_ne_zero

added theorem bernsteinPolynomial.iterate_derivative_at_1

added theorem bernsteinPolynomial.iterate_derivative_at_1_eq_zero_of_lt

added theorem bernsteinPolynomial.iterate_derivative_at_1_ne_zero

added theorem bernsteinPolynomial.iterate_derivative_succ_at_0_eq_zero

added theorem bernsteinPolynomial.linearIndependent

added theorem bernsteinPolynomial.linearIndependent_aux

added theorem bernsteinPolynomial.map

added theorem bernsteinPolynomial.sum

added theorem bernsteinPolynomial.sum_mul_smul

added theorem bernsteinPolynomial.sum_smul

added theorem bernsteinPolynomial.variance

added def bernsteinPolynomial