Theorems · Theorem · ring theory
SkewPolynomial.sum_eq_of_subset
∀ {R : Type u_1} [inst : Semiring R] {S : Type u_5} [inst_1 : AddCommMonoid S] {p : SkewPolynomial R} (f : ℕ → R → S),
(∀ (i : ℕ), f i 0 = 0) → ∀ {s : Finset ℕ}, p.support ⊆ s → p.sum f = ∑ n ∈ s, f n (p.coeff n)- Defined in
- Mathlib.Algebra.SkewPolynomial.Basic
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SemiringAddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- Finsetstatement and proof · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- Finset.sumstatement and proof · cited by 5,195
- SkewPolynomialstatement and proof · cited by 124
- Finset.sum_subsetproof · cited by 79
- SkewPolynomial.coeffstatement and proof · cited by 37
- SkewPolynomial.supportstatement and proof · cited by 30
- SkewPolynomial.sumstatement · cited by 22
- SkewPolynomial.sum_defproof · cited by 3
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.