Theorems · Theorem · field theory

Polynomial.aeval_sumIDeriv_of_pos

∀ {R : Type u_1} [inst : CommSemiring R] (A : Type u_3) [inst_1 : CommRing A] [inst_2 : Algebra R A] [Nontrivial A]
  [NoZeroDivisors A] (p : Polynomial R) {q : ℕ},
  0 < q →
    Function.Injective ⇑(algebraMap R A) →
      ∃ gp,
        gp.natDegree ≤ p.natDegree - q ∧
          ∀ (r : A) {p' : Polynomial A},
            Polynomial.map (algebraMap R A) p = (Polynomial.X - Polynomial.C r) ^ (q - 1) * p' →
              (Polynomial.aeval r) (Polynomial.sumIDeriv p) =
                (q - 1).factorial • Polynomial.eval r p' + q.factorial • (Polynomial.aeval r) gp

Defined in

Mathlib.Algebra.Polynomial.SumIteratedDerivative

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommRingAlgebraNontrivialNoZeroDivisors