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], ℝ)`.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
