Theorems · Theorem · commutative algebra

bernsteinPolynomial.derivative_succ_aux

∀ (R : Type u_1) [inst : CommRing R] (n ν : ℕ),
  Polynomial.derivative (bernsteinPolynomial R (n + 1) (ν + 1)) =
    (↑n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))

Defined in

Mathlib.RingTheory.Polynomial.Bernstein

Cited by

1 results in Mathlib

Foundations

Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing