Theorems · Theorem · ring theory

Finset.prod_add_ordered

∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] [inst_1 : LinearOrder ι] (s : Finset ι) (f g : ι → R),
  ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j

∏ i, (f i + g i) = (∏ i, f i) + ∑ i, g i * (∏ j < i, f j + g j) * (∏ j > i, f j).

Defined in

Mathlib.Algebra.BigOperators.Ring.Finset

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringLinearOrder