Theorems · Theorem · field theory

Polynomial.taylor_monomial

∀ {R : Type u_1} [inst : Semiring R] (r : R) (i : ℕ) (k : R),
  (Polynomial.taylor r) ((Polynomial.monomial i) k) = Polynomial.C k * (Polynomial.X + Polynomial.C r) ^ i

Defined in

Mathlib.Algebra.Polynomial.Taylor

Cited by

1 results in Mathlib

Foundations

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

Assumes

Semiring