Theorems · Definition · ring theory

SkewPolynomial.sum

{R : Type u_1} → [inst : Semiring R] → {S : Type u_5} → [AddCommMonoid S] → SkewPolynomial R → (ℕ → R → S) → S

p.sum f is ∑ n ∈ p.support, f n (p.coeff n), i.e., one sums the values of functions applied to coefficients of the polynomial p.

Defined in

Mathlib.Algebra.SkewPolynomial.Basic

Cited by

22 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoid