Theorems · Theorem · field theory

Polynomial.iterate_derivative_derivative_mul_X

∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} (p : Polynomial R),
  (⇑Polynomial.derivative)^[n] (Polynomial.derivative p * Polynomial.X) =
    (⇑Polynomial.derivative)^[n + 1] p * Polynomial.X + n • (⇑Polynomial.derivative)^[n] p

Defined in: Mathlib.Algebra.Polynomial.Derivative
Cited by: 2 results in Mathlib
Foundations: Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites37

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
RingHom.idstatement · cited by 18,349
CommSemiringstatement and proof · cited by 10,911
LinearMapstatement · cited by 10,215
Polynomialstatement and proof · cited by 5,681
Finset.sumproof · cited by 5,195
mul_oneproof · cited by 3,885
one_mulproof · cited by 2,841
add_zeroproof · cited by 2,707
Nat.cast_oneproof · cited by 2,501
zero_addproof · cited by 2,366
Finset.sum_congrproof · cited by 2,323

Cited by2

Results whose statement or proof uses this declaration.

Polynomial.Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eq_poly_in_Tproof · cited by 1
Polynomial.Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_eq_poly_in_Uproof · cited by 1