Theorems · Theorem · ring theory

SkewPolynomial.sum_def

∀ {R : Type u_1} [inst : Semiring R] {S : Type u_5} [inst_1 : AddCommMonoid S] (p : SkewPolynomial R) (f : ℕ → R → S),
  p.sum f = ∑ n ∈ p.support, f n (p.coeff n)

Defined in

Mathlib.Algebra.SkewPolynomial.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoid