Commit 2021-03-21 03:35 b75ec5cf

feat(data/polynomial): Bernstein polynomials (#6465) The definition of the Bernstein polynomials bernstein_polynomial (R : Type*) [ring R] (n ν : ℕ) : polynomial R := (choose n ν) * X^ν * (1 - X)^(n - ν) and the fact that for ν : fin (n+1) these are linearly independent over ℚ. (Future work: use these to prove Weierstrass' theorem that polynomials are dense in C([0,1], ℝ).