Theorems · Theorem · field theory

Polynomial.sum_add_index

∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : AddCommMonoid S] (p q : Polynomial R) (f : ℕ → R → S),
  (∀ (i : ℕ), f i 0 = 0) → (∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂) → (p + q).sum f = p.sum f + q.sum f

Defined in

Mathlib.Algebra.Polynomial.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoid