Mathlib.Algebra.BigOperators.Ring.Finset

Finset.prod_neg theorem

[CommMonoid α] [HasDistribNeg α] : ∏ x ∈ s, -f x = (-1) ^ #s * ∏ x ∈ s, f x

Full source

lemma prod_neg [CommMonoid α] [HasDistribNeg α] : ∏ x ∈ s, -f x = (-1) ^ #s * ∏ x ∈ s, f x := by
  simpa using (s.1.map f).prod_map_neg

Product of Negations Formula: $\prod_{x \in s} (-f(x)) = (-1)^{|s|} \prod_{x \in s} f(x)$

Informal description

Let $\alpha$ be a commutative monoid with a distributive negation operation. For any finite set $s$ and function $f : \alpha \to \alpha$, the product of the negations of $f$ over $s$ equals $(-1)^{|s|}$ multiplied by the product of $f$ over $s$, i.e., \[ \prod_{x \in s} (-f(x)) = (-1)^{|s|} \prod_{x \in s} f(x). \]

Finset.natCast_card_filter theorem

(p) [DecidablePred p] (s : Finset ι) : (#({x ∈ s | p x}) : α) = ∑ a ∈ s, if p a then (1 : α) else 0

Full source

lemma natCast_card_filter (p) [DecidablePred p] (s : Finset ι) :
    (#{x ∈ s | p x} : α) = ∑ a ∈ s, if p a then (1 : α) else 0 := by
  rw [sum_ite, sum_const_zero, add_zero, sum_const, nsmul_one]

Cardinality of Filtered Set as Sum of Indicators: $\#\{x \in s \mid p(x)\} = \sum_{a \in s} \mathbb{1}_p(a)$

Informal description

Let $\alpha$ be an additive commutative monoid with one, and let $s$ be a finite set of type $\iota$. For any decidable predicate $p$ on $\iota$, the cardinality of the filtered subset $\{x \in s \mid p(x)\}$, when viewed as an element of $\alpha$, is equal to the sum over $s$ of the indicator function for $p$, i.e., \[ \#\{x \in s \mid p(x)\} = \sum_{a \in s} \begin{cases} 1 & \text{if } p(a) \\ 0 & \text{otherwise} \end{cases}. \]

Finset.sum_boole theorem

(p) [DecidablePred p] (s : Finset ι) : (∑ x ∈ s, if p x then 1 else 0 : α) = #({x ∈ s | p x})

Full source

@[simp] lemma sum_boole (p) [DecidablePred p] (s : Finset ι) :
    (∑ x ∈ s, if p x then 1 else 0 : α) = #{x ∈ s | p x} :=
  (natCast_card_filter _ _).symm

Sum of Indicators Equals Cardinality of Filtered Set: $\sum_{x \in s} \mathbb{1}_p(x) = \#\{x \in s \mid p(x)\}$

Informal description

Let $\alpha$ be an additive commutative monoid with one, and let $s$ be a finite set of type $\iota$. For any decidable predicate $p$ on $\iota$, the sum over $s$ of the indicator function for $p$ equals the cardinality of the filtered subset $\{x \in s \mid p(x)\}$, i.e., \[ \sum_{x \in s} \begin{cases} 1 & \text{if } p(x) \\ 0 & \text{otherwise} \end{cases} = \#\{x \in s \mid p(x)\}. \]

Finset.sum_mul theorem

(s : Finset ι) (f : ι → α) (a : α) : (∑ i ∈ s, f i) * a = ∑ i ∈ s, f i * a

Full source

lemma sum_mul (s : Finset ι) (f : ι → α) (a : α) :
    (∑ i ∈ s, f i) * a = ∑ i ∈ s, f i * a := map_sum (AddMonoidHom.mulRight a) _ s

Distributivity of Summation over Multiplication: $(\sum_{i \in s} f(i)) \cdot a = \sum_{i \in s} (f(i) \cdot a)$

Informal description

For any finite set $s$ of type $\iota$, any function $f \colon \iota \to \alpha$, and any element $a \in \alpha$, the product of the sum $\sum_{i \in s} f(i)$ with $a$ is equal to the sum $\sum_{i \in s} (f(i) \cdot a)$.

Finset.mul_sum theorem

(s : Finset ι) (f : ι → α) (a : α) : a * ∑ i ∈ s, f i = ∑ i ∈ s, a * f i

Full source

lemma mul_sum (s : Finset ι) (f : ι → α) (a : α) :
    a * ∑ i ∈ s, f i = ∑ i ∈ s, a * f i := map_sum (AddMonoidHom.mulLeft a) _ s

Distributivity of Scalar Multiplication over Finite Sum

Informal description

For any finite set $s$ of type $\iota$, any function $f \colon \iota \to \alpha$, and any element $a \in \alpha$, the product of $a$ with the sum of $f$ over $s$ is equal to the sum over $s$ of $a$ multiplied by $f(i)$ for each $i \in s$. In symbols: $$ a \cdot \left( \sum_{i \in s} f(i) \right) = \sum_{i \in s} (a \cdot f(i)). $$

Finset.sum_mul_sum theorem

 {κ : Type*} (s : Finset ι) (t : Finset κ) (f : ι → α) (g : κ → α) :
  (∑ i ∈ s, f i) * ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i * g j

Full source

lemma sum_mul_sum {κ : Type*} (s : Finset ι) (t : Finset κ) (f : ι → α) (g : κ → α) :
    (∑ i ∈ s, f i) * ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i * g j := by
  simp_rw [sum_mul, ← mul_sum]

Product of Finite Sums Equals Double Sum of Products: $(\sum_{i \in s} f(i)) \cdot (\sum_{j \in t} g(j)) = \sum_{i \in s} \sum_{j \in t} (f(i) \cdot g(j))$

Informal description

For any finite sets $s \subseteq \iota$ and $t \subseteq \kappa$, and any functions $f \colon \iota \to \alpha$ and $g \colon \kappa \to \alpha$, the product of the sums $\sum_{i \in s} f(i)$ and $\sum_{j \in t} g(j)$ is equal to the double sum $\sum_{i \in s} \sum_{j \in t} (f(i) \cdot g(j))$.

Fintype.sum_mul_sum theorem

 {κ : Type*} [Fintype ι] [Fintype κ] (f : ι → α) (g : κ → α) : (∑ i, f i) * ∑ j, g j = ∑ i, ∑ j, f i * g j

Full source

lemma _root_.Fintype.sum_mul_sum {κ : Type*} [Fintype ι] [Fintype κ] (f : ι → α) (g : κ → α) :
    (∑ i, f i) * ∑ j, g j = ∑ i, ∑ j, f i * g j :=
  Finset.sum_mul_sum _ _ _ _

Product of Sums over Finite Types Equals Double Sum of Products: $(\sum_i f(i)) \cdot (\sum_j g(j)) = \sum_i \sum_j (f(i) \cdot g(j))$

Informal description

For any finite types $\iota$ and $\kappa$, and any functions $f \colon \iota \to \alpha$ and $g \colon \kappa \to \alpha$, the product of the sums $\sum_{i \in \iota} f(i)$ and $\sum_{j \in \kappa} g(j)$ is equal to the double sum $\sum_{i \in \iota} \sum_{j \in \kappa} (f(i) \cdot g(j))$.

Commute.sum_right theorem

(s : Finset ι) (f : ι → α) (b : α) (h : ∀ i ∈ s, Commute b (f i)) : Commute b (∑ i ∈ s, f i)

Full source

lemma _root_.Commute.sum_right (s : Finset ι) (f : ι → α) (b : α)
    (h : ∀ i ∈ s, Commute b (f i)) : Commute b (∑ i ∈ s, f i) :=
  (Commute.multiset_sum_right _ _) fun b hb => by
    obtain ⟨i, hi, rfl⟩ := Multiset.mem_map.mp hb
    exact h _ hi

Commutation of Element with Sum under Pairwise Commutation

Informal description

Let $S$ be a set with a multiplicative structure, and let $s$ be a finite subset of a type $\iota$. Given a function $f \colon \iota \to S$ and an element $b \in S$, if $b$ commutes with $f(i)$ for every $i \in s$, then $b$ commutes with the sum $\sum_{i \in s} f(i)$.

Commute.sum_left theorem

(s : Finset ι) (f : ι → α) (b : α) (h : ∀ i ∈ s, Commute (f i) b) : Commute (∑ i ∈ s, f i) b

Full source

lemma _root_.Commute.sum_left (s : Finset ι) (f : ι → α) (b : α)
    (h : ∀ i ∈ s, Commute (f i) b) : Commute (∑ i ∈ s, f i) b :=
  ((Commute.sum_right _ _ _) fun _i hi => (h _ hi).symm).symm

Sum Commutes with Element under Pairwise Commutation

Informal description

Let $S$ be a set with a multiplicative structure, and let $s$ be a finite subset of a type $\iota$. Given a function $f \colon \iota \to S$ and an element $b \in S$, if $f(i)$ commutes with $b$ for every $i \in s$, then the sum $\sum_{i \in s} f(i)$ commutes with $b$.

Finset.sum_range_succ_mul_sum_range_succ theorem

 (m n : ℕ) (f g : ℕ → α) :
  (∑ i ∈ range (m + 1), f i) * ∑ i ∈ range (n + 1), g i =
    (∑ i ∈ range m, f i) * ∑ i ∈ range n, g i + f m * ∑ i ∈ range n, g i + (∑ i ∈ range m, f i) * g n + f m * g n

Full source

lemma sum_range_succ_mul_sum_range_succ (m n : ℕ) (f g : ℕ → α) :
    (∑ i ∈ range (m + 1), f i) * ∑ i ∈ range (n + 1), g i =
      (∑ i ∈ range m, f i) * ∑ i ∈ range n, g i +
        f m * ∑ i ∈ range n, g i + (∑ i ∈ range m, f i) * g n + f m * g n := by
  simp only [add_mul, mul_add, add_assoc, sum_range_succ]

Expansion of Product of Sums over Successor Ranges

Informal description

For any natural numbers $m, n$ and functions $f, g \colon \mathbb{N} \to \alpha$ where $\alpha$ is a semiring, the product of the sums $\sum_{i=0}^m f(i)$ and $\sum_{j=0}^n g(j)$ can be expanded as: \[ \left(\sum_{i=0}^m f(i)\right) \left(\sum_{j=0}^n g(j)\right) = \left(\sum_{i=0}^{m-1} f(i)\right) \left(\sum_{j=0}^{n-1} g(j)\right) + f(m) \left(\sum_{j=0}^{n-1} g(j)\right) + \left(\sum_{i=0}^{m-1} f(i)\right) g(n) + f(m) g(n) \]

Finset.dvd_sum theorem

(h : ∀ i ∈ s, a ∣ f i) : a ∣ ∑ i ∈ s, f i

Full source

lemma dvd_sum (h : ∀ i ∈ s, a ∣ f i) : a ∣ ∑ i ∈ s, f i :=
  Multiset.dvd_sum fun y hy => by rcases Multiset.mem_map.1 hy with ⟨x, hx, rfl⟩; exact h x hx

Divisibility of Sum by Common Divisor in Finite Sets

Informal description

For any finite set $s$ and any function $f$ from elements of $s$ to a semiring $\alpha$, if an element $a \in \alpha$ divides $f(i)$ for every $i \in s$, then $a$ divides the sum $\sum_{i \in s} f(i)$.

Finset.sum_mul_boole theorem

(s : Finset ι) (f : ι → α) (i : ι) : ∑ j ∈ s, f j * ite (i = j) 1 0 = ite (i ∈ s) (f i) 0

Full source

lemma sum_mul_boole (s : Finset ι) (f : ι → α) (i : ι) :
    ∑ j ∈ s, f j * ite (i = j) 1 0 = ite (i ∈ s) (f i) 0 := by simp

Sum of Function Multiplied by Indicator Equals Function Value or Zero

Informal description

For any finite set $s$ of type $\iota$, any function $f \colon \iota \to \alpha$ where $\alpha$ is a semiring, and any element $i \in \iota$, the sum $\sum_{j \in s} f(j) \cdot \mathbb{1}_{i=j}$ equals $f(i)$ if $i \in s$ and $0$ otherwise. Here $\mathbb{1}_{i=j}$ denotes the indicator function which is $1$ when $i = j$ and $0$ otherwise.

Finset.sum_boole_mul theorem

(s : Finset ι) (f : ι → α) (i : ι) : ∑ j ∈ s, ite (i = j) 1 0 * f j = ite (i ∈ s) (f i) 0

Full source

lemma sum_boole_mul (s : Finset ι) (f : ι → α) (i : ι) :
    ∑ j ∈ s, ite (i = j) 1 0 * f j = ite (i ∈ s) (f i) 0 := by simp

Sum of Indicator-Weighted Function Values over Finite Set

Informal description

For any finite set $s$ indexed by $\iota$, any function $f \colon \iota \to \alpha$, and any index $i \in \iota$, the sum over $s$ of the terms $\mathbb{1}_{\{i = j\}} \cdot f(j)$ equals $f(i)$ if $i \in s$ and $0$ otherwise. Here $\mathbb{1}_{\{i = j\}}$ denotes the indicator function which is $1$ when $i = j$ and $0$ otherwise.

Finset.prod_add_prod_eq theorem

 {s : Finset ι} {i : ι} {f g h : ι → α} (hi : i ∈ s) (h1 : g i + h i = f i) (h2 : ∀ j ∈ s, j ≠ i → g j = f j)
  (h3 : ∀ j ∈ s, j ≠ i → h j = f j) : (∏ i ∈ s, g i) + ∏ i ∈ s, h i = ∏ i ∈ s, f i

Full source

/-- If `f = g = h` everywhere but at `i`, where `f i = g i + h i`, then the product of `f` over `s`
  is the sum of the products of `g` and `h`. -/
theorem prod_add_prod_eq {s : Finset ι} {i : ι} {f g h : ι → α} (hi : i ∈ s)
    (h1 : g i + h i = f i) (h2 : ∀ j ∈ s, j ≠ i → g j = f j) (h3 : ∀ j ∈ s, j ≠ i → h j = f j) :
    (∏ i ∈ s, g i) + ∏ i ∈ s, h i = ∏ i ∈ s, f i := by
  classical
    simp_rw [prod_eq_mul_prod_diff_singleton hi, ← h1, right_distrib]
    congr 2 <;> apply prod_congr rfl <;> simpa

Additive Decomposition of Products over Finite Sets

Informal description

Let $s$ be a finite set indexed by $\iota$, and let $f, g, h \colon \iota \to \alpha$ be functions where $\alpha$ is a semiring. Suppose there exists an element $i \in s$ such that: 1. $g(i) + h(i) = f(i)$, 2. For all $j \in s$ with $j \neq i$, we have $g(j) = f(j)$, 3. For all $j \in s$ with $j \neq i$, we have $h(j) = f(j)$. Then the sum of the products of $g$ and $h$ over $s$ equals the product of $f$ over $s$, i.e., \[ \prod_{j \in s} g(j) + \prod_{j \in s} h(j) = \prod_{j \in s} f(j). \]

Finset.prod_sum theorem

 (s : Finset ι) (t : ∀ i, Finset (κ i)) (f : ∀ i, κ i → α) :
  ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f x.1 (p x.1 x.2)

Full source

/-- The product over a sum can be written as a sum over the product of sets, `Finset.Pi`.
  `Finset.prod_univ_sum` is an alternative statement when the product is over `univ`. -/
lemma prod_sum (s : Finset ι) (t : ∀ i, Finset (κ i)) (f : ∀ i, κ i → α) :
    ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f x.1 (p x.1 x.2) := by
  classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    have h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y →
      Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t)) := by
      intro x _ y _ h
      simp only [disjoint_iff_ne, mem_image]
      rintro _ ⟨p₂, _, eq₂⟩ _ ⟨p₃, _, eq₃⟩ eq
      have : Pi.cons s a x p₂ a (mem_insert_self _ _)
              = Pi.cons s a y p₃ a (mem_insert_self _ _) := by rw [eq₂, eq₃, eq]
      rw [Pi.cons_same, Pi.cons_same] at this
      exact h this
    rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_biUnion h₁]
    refine sum_congr rfl fun b _ => ?_
    have h₂ : ∀ p₁ ∈ pi s t, ∀ p₂ ∈ pi s t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂ :=
      fun p₁ _ p₂ _ eq => Pi.cons_injective ha eq
    rw [sum_image h₂, mul_sum]
    refine sum_congr rfl fun g _ => ?_
    rw [attach_insert, prod_insert, prod_image]
    · simp only [Pi.cons_same]
      congr with ⟨v, hv⟩
      congr
      exact (Pi.cons_ne (by rintro rfl; exact ha hv)).symm
    · exact fun _ _ _ _ => Subtype.eqSubtype.eq ∘ Subtype.mk.inj
    · simpa only [mem_image, mem_attach, Subtype.mk.injEq, true_and,
        Subtype.exists, exists_prop, exists_eq_right] using ha

Product of Sums Equals Sum of Products over Finite Sets

Informal description

Let $s$ be a finite set indexed by $\iota$, and for each $i \in \iota$, let $t(i)$ be a finite set indexed by $\kappa(i)$. Given a function $f \colon \forall i, \kappa(i) \to \alpha$, the product over $s$ of the sums of $f(i, b)$ over $t(i)$ equals the sum over the cartesian product $\prod_{i \in s} t(i)$ of the products of $f(x, p(x))$ over the attached set $s.\text{attach}$. In symbols: \[ \prod_{i \in s} \left( \sum_{j \in t(i)} f(i, j) \right) = \sum_{p \in \prod_{i \in s} t(i)} \prod_{x \in s.\text{attach}} f(x.1, p(x.1, x.2)). \]

Finset.prod_univ_sum theorem

 [Fintype ι] (t : ∀ i, Finset (κ i)) (f : ∀ i, κ i → α) : ∏ i, ∑ j ∈ t i, f i j = ∑ x ∈ piFinset t, ∏ i, f i (x i)

Full source

/-- The product over `univ` of a sum can be written as a sum over the product of sets,
`Fintype.piFinset`. `Finset.prod_sum` is an alternative statement when the product is not
over `univ`. -/
lemma prod_univ_sum [Fintype ι] (t : ∀ i, Finset (κ i)) (f : ∀ i, κ i → α) :
    ∏ i, ∑ j ∈ t i, f i j = ∑ x ∈ piFinset t, ∏ i, f i (x i) := by
  simp only [prod_attach_univ, prod_sum, Finset.sum_univ_pi]

Product of Sums Equals Sum of Products over Finite Index Type

Informal description

Let $\iota$ be a finite type and $\alpha$ a commutative semiring. For each $i \in \iota$, let $t(i)$ be a finite set indexed by $\kappa(i)$, and let $f \colon \forall i, \kappa(i) \to \alpha$ be a function. Then the product over $\iota$ of the sums of $f(i,j)$ over $t(i)$ equals the sum over the finite product set $\prod_{i \in \iota} t(i)$ of the products of $f(i, x(i))$ over $\iota$. In symbols: \[ \prod_{i \in \iota} \left( \sum_{j \in t(i)} f(i,j) \right) = \sum_{x \in \prod_{i \in \iota} t(i)} \prod_{i \in \iota} f(i, x(i)). \]

Finset.sum_prod_piFinset theorem

 {κ : Type*} [Fintype ι] (s : Finset κ) (g : ι → κ → α) :
  ∑ f ∈ piFinset fun _ : ι ↦ s, ∏ i, g i (f i) = ∏ i, ∑ j ∈ s, g i j

Full source

lemma sum_prod_piFinset {κ : Type*} [Fintype ι] (s : Finset κ) (g : ι → κ → α) :
    ∑ f ∈ piFinset fun _ : ι ↦ s, ∏ i, g i (f i) = ∏ i, ∑ j ∈ s, g i j := by
  rw [← prod_univ_sum]

Sum-Product Interchange over Finite Function Space

Informal description

Let $\iota$ be a finite type, $\kappa$ a type, and $\alpha$ a commutative semiring. For a finite set $s \subseteq \kappa$ and a function $g \colon \iota \times \kappa \to \alpha$, the sum over all functions $f \colon \iota \to s$ of the product $\prod_{i \in \iota} g(i, f(i))$ equals the product over $\iota$ of the sums $\sum_{j \in s} g(i, j)$. In symbols: \[ \sum_{f \in s^\iota} \prod_{i \in \iota} g(i, f(i)) = \prod_{i \in \iota} \sum_{j \in s} g(i, j). \]

Finset.sum_pow' theorem

 (s : Finset ι') (f : ι' → α) (n : ℕ) : (∑ a ∈ s, f a) ^ n = ∑ p ∈ piFinset fun _i : Fin n ↦ s, ∏ i, f (p i)

Full source

lemma sum_pow' (s : Finset ι') (f : ι' → α) (n : ℕ) :
    (∑ a ∈ s, f a) ^ n = ∑ p ∈ piFinset fun _i : Fin n ↦ s, ∏ i, f (p i) := by
  convert @prod_univ_sum (Fin n) _ _ _ _ _ (fun _i ↦ s) fun _i d ↦ f d; simp

Power of Sum as Sum of Products over Finite Functions: $(\sum_{a \in s} f(a))^n = \sum_{p \in s^n} \prod_{i=1}^n f(p(i))$

Informal description

Let $s$ be a finite set indexed by $\iota'$, $f \colon \iota' \to \alpha$ a function where $\alpha$ is a commutative semiring, and $n$ a natural number. Then the $n$-th power of the sum of $f$ over $s$ equals the sum over all functions $p \colon \mathrm{Fin}(n) \to s$ of the product of $f(p(i))$ over $i \in \mathrm{Fin}(n)$. In symbols: \[ \left( \sum_{a \in s} f(a) \right)^n = \sum_{p \in s^{\mathrm{Fin}(n)}} \prod_{i \in \mathrm{Fin}(n)} f(p(i)). \]

Finset.prod_add theorem

 (f g : ι → α) (s : Finset ι) : ∏ i ∈ s, (f i + g i) = ∑ t ∈ s.powerset, (∏ i ∈ t, f i) * ∏ i ∈ s \ t, g i

Full source

/-- The product of `f a + g a` over all of `s` is the sum over the powerset of `s` of the product of
`f` over a subset `t` times the product of `g` over the complement of `t` -/
theorem prod_add (f g : ι → α) (s : Finset ι) :
    ∏ i ∈ s, (f i + g i) = ∑ t ∈ s.powerset, (∏ i ∈ t, f i) * ∏ i ∈ s \ t, g i := by
  classical
  calc
    ∏ i ∈ s, (f i + g i) =
        ∏ i ∈ s, ∑ p ∈ ({True, False} : Finset Prop), if p then f i else g i := by simp
    _ = ∑ p ∈ (s.pi fun _ => {True, False} : Finset (∀ a ∈ s, Prop)),
          ∏ a ∈ s.attach, if p a.1 a.2 then f a.1 else g a.1 := prod_sum _ _ _
    _ = ∑ t ∈ s.powerset, (∏ a ∈ t, f a) * ∏ a ∈ s \ t, g a :=
      sum_bij'
        (fun f _ ↦ {a ∈ s | ∃ h : a ∈ s, f a h})
        (fun t _ a _ => a ∈ t)
        (by simp)
        (by simp [Classical.em])
        (by simp_rw [mem_filter, funext_iff, eq_iff_iff, mem_pi, mem_insert]; tauto)
        (by simp_rw [Finset.ext_iff, @mem_filter _ _ (id _), mem_powerset]; tauto)
        (fun a _ ↦ by
          simp only [prod_ite, filter_attach', prod_map, Function.Embedding.coeFn_mk,
            Subtype.map_coe, id_eq, prod_attach, filter_congr_decidable]
          congr 2 with x
          simp only [mem_filter, mem_sdiff, not_and, not_exists, and_congr_right_iff]
          tauto)

Product of Sums Decomposition via Power Set

Informal description

Let $s$ be a finite set indexed by $\iota$, and let $f, g \colon \iota \to \alpha$ be functions where $\alpha$ is a commutative semiring. The product over $s$ of the sums $(f(i) + g(i))$ equals the sum over all subsets $t \subseteq s$ of the product of $f$ over $t$ multiplied by the product of $g$ over the complement $s \setminus t$. In symbols: \[ \prod_{i \in s} (f(i) + g(i)) = \sum_{t \subseteq s} \left( \prod_{i \in t} f(i) \right) \left( \prod_{i \in s \setminus t} g(i) \right). \]

Finset.prod_one_add theorem

{f : ι → α} (s : Finset ι) : ∏ i ∈ s, (1 + f i) = ∑ t ∈ s.powerset, ∏ i ∈ t, f i

Full source

theorem prod_one_add {f : ι → α} (s : Finset ι) :
    ∏ i ∈ s, (1 + f i) = ∑ t ∈ s.powerset, ∏ i ∈ t, f i := by
  classical simp only [add_comm (1 : α), prod_add, prod_const_one, mul_one]

Product-to-Sum Expansion for $(1 + f(i))$ over Finite Sets

Informal description

For any finite set $s$ indexed by $\iota$ and any function $f \colon \iota \to \alpha$ where $\alpha$ is a commutative semiring, the product over $s$ of the terms $(1 + f(i))$ equals the sum over all subsets $t \subseteq s$ of the product of $f$ over $t$. In symbols: \[ \prod_{i \in s} (1 + f(i)) = \sum_{t \subseteq s} \prod_{i \in t} f(i). \]

Finset.prod_add_one theorem

{f : ι → α} (s : Finset ι) : ∏ i ∈ s, (f i + 1) = ∑ t ∈ s.powerset, ∏ i ∈ t, f i

Full source

theorem prod_add_one {f : ι → α} (s : Finset ι) :
    ∏ i ∈ s, (f i + 1) = ∑ t ∈ s.powerset, ∏ i ∈ t, f i := by
  classical simp only [prod_add, prod_const_one, mul_one]

Product-to-Sum Identity for $(f(i)+1)$ over Finite Sets

Informal description

For any finite set $s$ indexed by $\iota$ and any function $f \colon \iota \to \alpha$ where $\alpha$ is a commutative semiring, the product over $s$ of the terms $(f(i) + 1)$ equals the sum over all subsets $t \subseteq s$ of the product of $f$ over $t$. In symbols: \[ \prod_{i \in s} (f(i) + 1) = \sum_{t \subseteq s} \prod_{i \in t} f(i). \]

Finset.prod_add_ordered theorem

 [LinearOrder ι] (s : Finset ι) (f g : ι → α) :
  ∏ 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

Full source

/-- `∏ i, (f i + g i) = (∏ i, f i) + ∑ i, g i * (∏ j < i, f j + g j) * (∏ j > i, f j)`. -/
theorem prod_add_ordered [LinearOrder ι] (s : Finset ι) (f g : ι → α) :
    ∏ 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 := by
  refine Finset.induction_on_max s (by simp) ?_
  clear s
  intro a s ha ihs
  have ha' : a ∉ s := fun ha' => lt_irrefl a (ha a ha')
  rw [prod_insert ha', prod_insert ha', sum_insert ha', filter_insert, if_neg (lt_irrefl a),
    filter_true_of_mem ha, ihs, add_mul, mul_add, mul_add, add_assoc]
  congr 1
  rw [add_comm]
  congr 1
  · rw [filter_false_of_mem, prod_empty, mul_one]
    exact (forall_mem_insert _ _ _).2 ⟨lt_irrefl a, fun i hi => (ha i hi).not_lt⟩
  · rw [mul_sum]
    refine sum_congr rfl fun i hi => ?_
    rw [filter_insert, if_neg (ha i hi).not_lt, filter_insert, if_pos (ha i hi), prod_insert,
      mul_left_comm]
    exact mt (fun ha => (mem_filter.1 ha).1) ha'

Ordered Product-Sum Expansion: $\prod (f + g) = \prod f + \sum g \cdot \prod_{<} (f + g) \cdot \prod_{>} f$

Informal description

Let $\iota$ be a linearly ordered type, $s$ a finite subset of $\iota$, and $f, g : \iota \to \alpha$ functions into a semiring $\alpha$. Then the product of $(f(i) + g(i))$ over $s$ can be expressed as: \[ \prod_{i \in s} (f(i) + g(i)) = \left(\prod_{i \in s} f(i)\right) + \sum_{i \in s} \left(g(i) \cdot \prod_{\substack{j \in s \\ j < i}} (f(j) + g(j)) \cdot \prod_{\substack{j \in s \\ i < j}} f(j)\right). \]

Finset.sum_pow_mul_eq_add_pow theorem

(a b : α) (s : Finset ι) : (∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t)) = (a + b) ^ #s

Full source

/-- Summing `a ^ #t * b ^ (n - #t)` over all finite subsets `t` of a finset `s`
gives `(a + b) ^ #s`. -/
theorem sum_pow_mul_eq_add_pow (a b : α) (s : Finset ι) :
    (∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t)) = (a + b) ^ #s := by
  classical
  rw [← prod_const, prod_add]
  refine Finset.sum_congr rfl fun t ht => ?_
  rw [prod_const, prod_const, ← card_sdiff (mem_powerset.1 ht)]

Binomial Expansion for Finite Sets: $\sum_{t \subseteq s} a^{\#t} b^{\#s - \#t} = (a + b)^{\#s}$

Informal description

Let $\alpha$ be a semiring, $s$ be a finite set indexed by $\iota$, and $a, b \in \alpha$. The sum over all subsets $t \subseteq s$ of $a$ raised to the cardinality of $t$ multiplied by $b$ raised to the cardinality of $s$ minus the cardinality of $t$ equals $(a + b)$ raised to the cardinality of $s$. In symbols: \[ \sum_{t \subseteq s} a^{\#t} \cdot b^{\#s - \#t} = (a + b)^{\#s}. \]

Fintype.sum_pow_mul_eq_add_pow theorem

 (ι : Type*) [Fintype ι] (a b : α) : ∑ s : Finset ι, a ^ #s * b ^ (Fintype.card ι - #s) = (a + b) ^ Fintype.card ι

Full source

/-- Summing `a^#s * b^(n-#s)` over all finite subsets `s` of a fintype of cardinality `n`
gives `(a + b)^n`. The "good" proof involves expanding along all coordinates using the fact that
`x^n` is multilinear, but multilinear maps are only available now over rings, so we give instead
a proof reducing to the usual binomial theorem to have a result over semirings. -/
lemma _root_.Fintype.sum_pow_mul_eq_add_pow (ι : Type*) [Fintype ι] (a b : α) :
    ∑ s : Finset ι, a ^ #s * b ^ (Fintype.card ι - #s) = (a + b) ^ Fintype.card ι :=
  Finset.sum_pow_mul_eq_add_pow _ _ _

Binomial Expansion for Finite Types: $\sum_{s \subseteq \iota} a^{\#s} b^{\#\iota - \#s} = (a + b)^{\#\iota}$

Informal description

Let $\alpha$ be a semiring, $\iota$ a finite type, and $a, b \in \alpha$. The sum over all finite subsets $s \subseteq \iota$ of $a$ raised to the cardinality of $s$ multiplied by $b$ raised to the cardinality of $\iota$ minus the cardinality of $s$ equals $(a + b)$ raised to the cardinality of $\iota$. In symbols: \[ \sum_{s \subseteq \iota} a^{\#s} \cdot b^{\#\iota - \#s} = (a + b)^{\#\iota}. \]

Finset.prod_natCast theorem

(s : Finset ι) (f : ι → ℕ) : ↑(∏ i ∈ s, f i : ℕ) = ∏ i ∈ s, (f i : α)

Full source

@[norm_cast]
theorem prod_natCast (s : Finset ι) (f : ι → ℕ) : ↑(∏ i ∈ s, f i : ℕ) = ∏ i ∈ s, (f i : α) :=
  map_prod (Nat.castRingHom α) f s

Canonical Homomorphism Commutes with Finite Product: $\left( \prod_{i \in s} f(i) \right) = \prod_{i \in s} f(i)$

Informal description

Let $s$ be a finite set of type $\iota$ and $f : \iota \to \mathbb{N}$ a function. Then the canonical ring homomorphism from $\mathbb{N}$ to a semiring $\alpha$ commutes with finite products, i.e., \[ \left( \prod_{i \in s} f(i) \right) = \prod_{i \in s} f(i), \] where the left-hand side is the natural number product and the right-hand side is the product in $\alpha$ via the canonical homomorphism.

Finset.prod_sub theorem

 [DecidableEq ι] (f g : ι → α) (s : Finset ι) :
  ∏ i ∈ s, (f i - g i) = ∑ t ∈ s.powerset, (-1) ^ #t * (∏ i ∈ s \ t, f i) * ∏ i ∈ t, g i

Full source

/-- The product of `f i - g i` over all of `s` is the sum over the powerset of `s` of the product of
`g` over a subset `t` times the product of `f` over the complement of `t` times `(-1) ^ #t`. -/
lemma prod_sub [DecidableEq ι] (f g : ι → α) (s : Finset ι) :
    ∏ i ∈ s, (f i - g i) = ∑ t ∈ s.powerset, (-1) ^ #t * (∏ i ∈ s \ t, f i) * ∏ i ∈ t, g i := by
  simp [sub_eq_neg_add, prod_add, prod_neg, mul_right_comm]

Product of Differences Formula via Power Set: $\prod_{i \in s} (f(i) - g(i)) = \sum_{t \subseteq s} (-1)^{|t|} \prod_{i \in s \setminus t} f(i) \prod_{i \in t} g(i)$

Informal description

Let $\alpha$ be a commutative ring, $\iota$ a type with decidable equality, $s$ a finite subset of $\iota$, and $f, g \colon \iota \to \alpha$ functions. Then the product of $(f(i) - g(i))$ over all $i \in s$ equals the sum over all subsets $t \subseteq s$ of $(-1)^{|t|}$ multiplied by the product of $f$ over $s \setminus t$ and the product of $g$ over $t$. In symbols: \[ \prod_{i \in s} (f(i) - g(i)) = \sum_{t \subseteq s} (-1)^{|t|} \left( \prod_{i \in s \setminus t} f(i) \right) \left( \prod_{i \in t} g(i) \right). \]

Finset.prod_sub_ordered theorem

 [LinearOrder ι] (s : Finset ι) (f g : ι → α) :
  ∏ 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

Full source

/-- `∏ i, (f i - g i) = (∏ i, f i) - ∑ i, g i * (∏ j < i, f j - g j) * (∏ j > i, f j)`. -/
lemma prod_sub_ordered [LinearOrder ι] (s : Finset ι) (f g : ι → α) :
    ∏ 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 := by
  simp only [sub_eq_add_neg]
  convert prod_add_ordered s f fun i => -g i
  simp

Ordered Product-Difference Expansion: $\prod (f - g) = \prod f - \sum g \cdot \prod_{<} (f - g) \cdot \prod_{>} f$

Informal description

Let $\iota$ be a linearly ordered type, $s$ a finite subset of $\iota$, and $f, g \colon \iota \to \alpha$ functions into a semiring $\alpha$. Then the product of $(f(i) - g(i))$ over $s$ can be expressed as: \[ \prod_{i \in s} (f(i) - g(i)) = \left(\prod_{i \in s} f(i)\right) - \sum_{i \in s} \left(g(i) \cdot \prod_{\substack{j \in s \\ j < i}} (f(j) - g(j)) \cdot \prod_{\substack{j \in s \\ i < j}} f(j)\right). \]

Finset.prod_one_sub_ordered theorem

 [LinearOrder ι] (s : Finset ι) (f : ι → α) : ∏ i ∈ s, (1 - f i) = 1 - ∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 - f j)

Full source

/-- `∏ i, (1 - f i) = 1 - ∑ i, f i * (∏ j < i, 1 - f j)`. This formula is useful in construction of
a partition of unity from a collection of “bump” functions. -/
theorem prod_one_sub_ordered [LinearOrder ι] (s : Finset ι) (f : ι → α) :
    ∏ i ∈ s, (1 - f i) = 1 - ∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 - f j) := by
  rw [prod_sub_ordered]
  simp

Product Expansion: $\prod (1 - f) = 1 - \sum f \cdot \prod_{<} (1 - f)$

Informal description

Let $\iota$ be a linearly ordered type, $s$ a finite subset of $\iota$, and $f \colon \iota \to \alpha$ a function into a semiring $\alpha$. Then the product of $(1 - f(i))$ over $s$ can be expressed as: \[ \prod_{i \in s} (1 - f(i)) = 1 - \sum_{i \in s} \left(f(i) \cdot \prod_{\substack{j \in s \\ j < i}} (1 - f(j))\right). \]

Finset.prod_range_natCast_sub theorem

(n k : ℕ) : ∏ i ∈ range k, (n - i : α) = (∏ i ∈ range k, (n - i) : ℕ)

Full source

theorem prod_range_natCast_sub (n k : ℕ) :
    ∏ i ∈ range k, (n - i : α) = (∏ i ∈ range k, (n - i) : ℕ) := by
  rw [prod_natCast]
  rcases le_or_lt k n with hkn | hnk
  · exact prod_congr rfl fun i hi => (Nat.cast_sub <| (mem_range.1 hi).le.trans hkn).symm
  · rw [← mem_range] at hnk
    rw [prod_eq_zero hnk, prod_eq_zero hnk] <;> simp

Natural number falling factorial product commutes with semiring cast: $\prod_{i=0}^{k-1} (n - i)_\alpha = \left(\prod_{i=0}^{k-1} (n - i)\right)_\mathbb{N}$

Informal description

For any natural numbers $n$ and $k$, and any semiring $\alpha$, the product $\prod_{i=0}^{k-1} (n - i)$ computed in $\alpha$ equals the natural number product $\prod_{i=0}^{k-1} (n - i)$ cast to $\alpha$.

Fintype.sum_pow theorem

(f : ι → α) (n : ℕ) : (∑ a, f a) ^ n = ∑ p : Fin n → ι, ∏ i, f (p i)

Full source

lemma sum_pow (f : ι → α) (n : ℕ) : (∑ a, f a) ^ n = ∑ p : Fin n → ι, ∏ i, f (p i) := by
  simp [sum_pow']

Power of Sum as Sum of Products over Finite Type: $(\sum_{a} f(a))^n = \sum_{p \colon \mathrm{Fin}(n) \to \iota} \prod_{i} f(p(i))$

Informal description

Let $\iota$ be a finite type and $\alpha$ a commutative semiring. For any function $f \colon \iota \to \alpha$ and natural number $n$, the $n$-th power of the sum of $f$ over $\iota$ equals the sum over all functions $p \colon \mathrm{Fin}(n) \to \iota$ of the product of $f(p(i))$ over $i \in \mathrm{Fin}(n)$. In symbols: \[ \left( \sum_{a \in \iota} f(a) \right)^n = \sum_{p \colon \mathrm{Fin}(n) \to \iota} \prod_{i \in \mathrm{Fin}(n)} f(p(i)). \]

Fintype.prod_sum theorem

 {κ : ι → Type*} [∀ i, Fintype (κ i)] (f : ∀ i, κ i → α) : ∏ i, ∑ j, f i j = ∑ x : ∀ i, κ i, ∏ i, f i (x i)

Full source

/-- A product of sums can be written as a sum of products. -/
lemma prod_sum {κ : ι → Type*} [∀ i, Fintype (κ i)] (f : ∀ i, κ i → α) :
    ∏ i, ∑ j, f i j = ∑ x : ∀ i, κ i, ∏ i, f i (x i) := Finset.prod_univ_sum _ _

Product of Sums Equals Sum of Products over Finite Index Types

Informal description

Let $\iota$ be a finite type and $\alpha$ a commutative semiring. For each $i \in \iota$, let $\kappa(i)$ be a finite type and $f \colon \forall i, \kappa(i) \to \alpha$ a function. Then the product over $\iota$ of the sums of $f(i,j)$ over all $j \in \kappa(i)$ equals the sum over all functions $x \colon \forall i, \kappa(i)$ of the products of $f(i, x(i))$ over $\iota$. In symbols: \[ \prod_{i \in \iota} \left( \sum_{j \in \kappa(i)} f(i,j) \right) = \sum_{x \colon \forall i, \kappa(i)} \prod_{i \in \iota} f(i, x(i)). \]

Fintype.prod_add theorem

(f g : ι → α) : ∏ a, (f a + g a) = ∑ t, (∏ a ∈ t, f a) * ∏ a ∈ tᶜ, g a

Full source

lemma prod_add (f g : ι → α) : ∏ a, (f a + g a) = ∑ t, (∏ a ∈ t, f a) * ∏ a ∈ tᶜ, g a := by
  simpa [compl_eq_univ_sdiff] using Finset.prod_add f g univ

Product of Sums Decomposition over Finite Type

Informal description

Let $\iota$ be a finite type and $\alpha$ a commutative semiring. For any functions $f, g \colon \iota \to \alpha$, the product over all elements $a \in \iota$ of $(f(a) + g(a))$ equals the sum over all subsets $t \subseteq \iota$ of the product of $f$ over $t$ multiplied by the product of $g$ over the complement $t^\complement$. In symbols: \[ \prod_{a \in \iota} (f(a) + g(a)) = \sum_{t \subseteq \iota} \left( \prod_{a \in t} f(a) \right) \left( \prod_{a \in t^\complement} g(a) \right). \]

Nat.sum_div theorem

(hf : ∀ i ∈ s, n ∣ f i) : (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n

Full source

protected lemma sum_div (hf : ∀ i ∈ s, n ∣ f i) : (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n := by
  obtain rfl | hn := n.eq_zero_or_pos
  · simp
  rw [Nat.div_eq_iff_eq_mul_left hn (dvd_sum hf), sum_mul]
  refine sum_congr rfl fun s hs ↦ ?_
  rw [Nat.div_mul_cancel (hf _ hs)]

Division Distributes over Sum of Divisible Terms in Natural Numbers

Informal description

For any finite set $s$, any function $f$ from elements of $s$ to natural numbers, and any natural number $n$ that divides $f(i)$ for all $i \in s$, the division of the sum $\sum_{i \in s} f(i)$ by $n$ equals the sum of the divisions $\sum_{i \in s} (f(i)/n)$.

Nat.cast_list_sum theorem

[AddMonoidWithOne β] (s : List ℕ) : (↑s.sum : β) = (s.map (↑)).sum

Full source

@[simp, norm_cast]
lemma cast_list_sum [AddMonoidWithOne β] (s : List ℕ) : (↑s.sum : β) = (s.map (↑)).sum :=
  map_list_sum (castAddMonoidHom β) _

Canonical Homomorphism Preserves Sum of List of Natural Numbers

Informal description

Let $\beta$ be an additive monoid with a multiplicative identity. For any list $s$ of natural numbers, the canonical homomorphism from $\mathbb{N}$ to $\beta$ applied to the sum of $s$ is equal to the sum of the list obtained by applying the canonical homomorphism to each element of $s$. In symbols: \[ \text{cast}(s.\text{sum}) = (s.\text{map}(\text{cast})).\text{sum} \]

Nat.cast_list_prod theorem

[Semiring β] (s : List ℕ) : (↑s.prod : β) = (s.map (↑)).prod

Full source

@[simp, norm_cast]
lemma cast_list_prod [Semiring β] (s : List ℕ) : (↑s.prod : β) = (s.map (↑)).prod :=
  map_list_prod (castRingHom β) _

Natural Number List Product Homomorphism: $(\prod x)_\beta = \prod x_\beta$

Informal description

Let $\beta$ be a semiring. For any list $s$ of natural numbers, the image of the product of $s$ under the canonical ring homomorphism from $\mathbb{N}$ to $\beta$ is equal to the product of the list obtained by applying the homomorphism to each element of $s$. That is, \[ \left(\prod_{x \in s} x\right)_\beta = \prod_{x \in s} x_\beta. \]

Nat.cast_multiset_sum theorem

[AddCommMonoidWithOne β] (s : Multiset ℕ) : (↑s.sum : β) = (s.map (↑)).sum

Full source

@[simp, norm_cast]
lemma cast_multiset_sum [AddCommMonoidWithOne β] (s : Multiset ℕ) :
    (↑s.sum : β) = (s.map (↑)).sum :=
  map_multiset_sum (castAddMonoidHom β) _

Canonical Homomorphism Preserves Sum of Multiset of Natural Numbers

Informal description

Let $\beta$ be an additive commutative monoid with one. For any multiset $s$ of natural numbers, the canonical homomorphism from $\mathbb{N}$ to $\beta$ applied to the sum of $s$ is equal to the sum of the multiset obtained by applying the canonical homomorphism to each element of $s$. In symbols: \[ \text{cast}(s.\text{sum}) = (s.\text{map}(\text{cast})).\text{sum} \]

Nat.cast_multiset_prod theorem

[CommSemiring β] (s : Multiset ℕ) : (↑s.prod : β) = (s.map (↑)).prod

Full source

@[simp, norm_cast]
lemma cast_multiset_prod [CommSemiring β] (s : Multiset ℕ) : (↑s.prod : β) = (s.map (↑)).prod :=
  map_multiset_prod (castRingHom β) _

Natural Number Multiset Product Homomorphism: $(\prod x)_\beta = \prod x_\beta$

Informal description

Let $\beta$ be a commutative semiring. For any multiset $s$ of natural numbers, the image of the product of $s$ under the canonical ring homomorphism from $\mathbb{N}$ to $\beta$ is equal to the product of the multiset obtained by applying the homomorphism to each element of $s$. That is, \[ \left(\prod_{x \in s} x\right)_\beta = \prod_{x \in s} x_\beta. \]

Nat.cast_sum theorem

[AddCommMonoidWithOne β] (s : Finset α) (f : α → ℕ) : ↑(∑ x ∈ s, f x : ℕ) = ∑ x ∈ s, (f x : β)

Full source

@[simp, norm_cast]
lemma cast_sum [AddCommMonoidWithOne β] (s : Finset α) (f : α → ℕ) :
    ↑(∑ x ∈ s, f x : ℕ) = ∑ x ∈ s, (f x : β) :=
  map_sum (castAddMonoidHom β) _ _

Sum Homomorphism Property for Natural Numbers to Additive Commutative Monoid with One

Informal description

Let $\beta$ be an additive commutative monoid with one, $s$ be a finite set indexed by $\alpha$, and $f : \alpha \to \mathbb{N}$ be a function. Then the canonical homomorphism from $\mathbb{N}$ to $\beta$ applied to the sum $\sum_{x \in s} f(x)$ equals the sum $\sum_{x \in s} (f(x) : \beta)$.

Nat.cast_prod theorem

[CommSemiring β] (f : α → ℕ) (s : Finset α) : (↑(∏ i ∈ s, f i) : β) = ∏ i ∈ s, (f i : β)

Full source

@[simp, norm_cast]
lemma cast_prod [CommSemiring β] (f : α → ℕ) (s : Finset α) :
    (↑(∏ i ∈ s, f i) : β) = ∏ i ∈ s, (f i : β) :=
  map_prod (castRingHom β) _ _

Product Homomorphism Property for Natural Numbers to Commutative Semiring

Informal description

Let $\beta$ be a commutative semiring, $s$ be a finite set indexed by $\alpha$, and $f : \alpha \to \mathbb{N}$ be a function. Then the canonical homomorphism from $\mathbb{N}$ to $\beta$ applied to the product $\prod_{i \in s} f(i)$ equals the product $\prod_{i \in s} (f(i) : \beta)$.

Int.sum_div theorem

(hf : ∀ i ∈ s, n ∣ f i) : (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n

Full source

protected lemma sum_div (hf : ∀ i ∈ s, n ∣ f i) : (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n := by
  obtain rfl | hn := eq_or_ne n 0
  · simp
  rw [Int.ediv_eq_iff_eq_mul_left hn (dvd_sum hf), sum_mul]
  refine sum_congr rfl fun s hs ↦ ?_
  rw [Int.ediv_mul_cancel (hf _ hs)]

Quotient of Sum by Common Divisor in Integers: $(\sum_{i \in s} f(i)) / n = \sum_{i \in s} (f(i) / n)$

Informal description

For any finite set $s$, any function $f$ from elements of $s$ to the integers $\mathbb{Z}$, and any integer $n$ such that $n$ divides $f(i)$ for every $i \in s$, the quotient of the sum $\sum_{i \in s} f(i)$ divided by $n$ is equal to the sum $\sum_{i \in s} (f(i) / n)$.

Int.cast_list_sum theorem

[AddGroupWithOne β] (s : List ℤ) : (↑s.sum : β) = (s.map (↑)).sum

Full source

@[simp, norm_cast]
lemma cast_list_sum [AddGroupWithOne β] (s : List ℤ) : (↑s.sum : β) = (s.map (↑)).sum :=
  map_list_sum (castAddHom β) _

Canonical Homomorphism Preserves Integer List Sums in Additive Groups with One

Informal description

Let $\beta$ be an additive group with one and $s$ be a list of integers. The image of the sum of $s$ under the canonical homomorphism from $\mathbb{Z}$ to $\beta$ is equal to the sum of the list obtained by applying the canonical homomorphism to each element of $s$. That is, \[ \left(\sum_{x \in s} x\right)_\beta = \sum_{x \in s} x_\beta \] where $x_\beta$ denotes the image of $x \in \mathbb{Z}$ in $\beta$ under the canonical homomorphism.

Int.cast_list_prod theorem

[Ring β] (s : List ℤ) : (↑s.prod : β) = (s.map (↑)).prod

Full source

@[simp, norm_cast]
lemma cast_list_prod [Ring β] (s : List ℤ) : (↑s.prod : β) = (s.map (↑)).prod :=
  map_list_prod (castRingHom β) _

Canonical Homomorphism Preserves Integer List Products in Rings

Informal description

Let $\beta$ be a ring and $s$ be a list of integers. The image of the product of $s$ under the canonical ring homomorphism from $\mathbb{Z}$ to $\beta$ is equal to the product of the list obtained by applying the canonical homomorphism to each element of $s$. That is, \[ \left(\prod_{x \in s} x\right)_\beta = \prod_{x \in s} x_\beta \] where $x_\beta$ denotes the image of $x \in \mathbb{Z}$ in $\beta$ under the canonical homomorphism.

Int.cast_multiset_sum theorem

[AddCommGroupWithOne β] (s : Multiset ℤ) : (↑s.sum : β) = (s.map (↑)).sum

Full source

@[simp, norm_cast]
lemma cast_multiset_sum [AddCommGroupWithOne β] (s : Multiset ℤ) :
    (↑s.sum : β) = (s.map (↑)).sum :=
  map_multiset_sum (castAddHom β) _

Canonical Homomorphism Preserves Integer Multiset Sums in Additive Commutative Groups with One

Informal description

Let $\beta$ be an additive commutative group with one. For any multiset $s$ of integers, the image of the sum of $s$ under the canonical additive group homomorphism from $\mathbb{Z}$ to $\beta$ is equal to the sum of the multiset obtained by applying the canonical homomorphism to each element of $s$. That is, \[ \left(\sum_{x \in s} x\right)_\beta = \sum_{x \in s} x_\beta \] where $x_\beta$ denotes the image of $x \in \mathbb{Z}$ in $\beta$ under the canonical homomorphism.

Int.cast_multiset_prod theorem

{R : Type*} [CommRing R] (s : Multiset ℤ) : (↑s.prod : R) = (s.map (↑)).prod

Full source

@[simp, norm_cast]
lemma cast_multiset_prod {R : Type*} [CommRing R] (s : Multiset ℤ) :
    (↑s.prod : R) = (s.map (↑)).prod :=
  map_multiset_prod (castRingHom R) _

Canonical Homomorphism Preserves Integer Multiset Products in Commutative Rings

Informal description

Let $R$ be a commutative ring. For any multiset $s$ of integers, the image of the product of $s$ under the canonical ring homomorphism from $\mathbb{Z}$ to $R$ is equal to the product of the multiset obtained by applying the canonical homomorphism to each element of $s$. That is, \[ \left(\prod_{x \in s} x\right)_R = \prod_{x \in s} x_R \] where $x_R$ denotes the image of $x \in \mathbb{Z}$ in $R$ under the canonical homomorphism.

Int.cast_sum theorem

[AddCommGroupWithOne β] (s : Finset α) (f : α → ℤ) : ↑(∑ x ∈ s, f x : ℤ) = ∑ x ∈ s, (f x : β)

Full source

@[simp, norm_cast]
lemma cast_sum [AddCommGroupWithOne β] (s : Finset α) (f : α → ℤ) :
    ↑(∑ x ∈ s, f x : ℤ) = ∑ x ∈ s, (f x : β) :=
  map_sum (castAddHom β) _ _

Canonical homomorphism commutes with finite sums: $(\sum f(x))_\beta = \sum (f(x))_\beta$

Informal description

Let $\beta$ be an additive commutative group with one. For any finite set $s$ of elements of type $\alpha$ and any function $f \colon \alpha \to \mathbb{Z}$, the image under the canonical homomorphism $\mathbb{Z} \to \beta$ of the sum $\sum_{x \in s} f(x)$ equals the sum $\sum_{x \in s} (f(x) : \beta)$. In other words, \[ \left(\sum_{x \in s} f(x)\right)_\beta = \sum_{x \in s} (f(x))_\beta \] where $(\cdot)_\beta$ denotes the image under the canonical homomorphism $\mathbb{Z} \to \beta$.

Int.cast_prod theorem

{R : Type*} [CommRing R] (f : α → ℤ) (s : Finset α) : (↑(∏ i ∈ s, f i) : R) = ∏ i ∈ s, (f i : R)

Full source

@[simp, norm_cast]
lemma cast_prod {R : Type*} [CommRing R] (f : α → ℤ) (s : Finset α) :
    (↑(∏ i ∈ s, f i) : R) = ∏ i ∈ s, (f i : R) :=
  map_prod (Int.castRingHom R) _ _

Canonical homomorphism commutes with finite products: $(\prod f(i))_R = \prod (f(i))_R$

Informal description

Let $R$ be a commutative ring and $\alpha$ be an arbitrary type. For any function $f \colon \alpha \to \mathbb{Z}$ and any finite subset $s \subset \alpha$, the image under the canonical ring homomorphism $\mathbb{Z} \to R$ of the product $\prod_{i \in s} f(i)$ equals the product $\prod_{i \in s} (f(i) : R)$ in $R$. In other words, \[ \left(\prod_{i \in s} f(i)\right)_R = \prod_{i \in s} (f(i))_R \] where $(\cdot)_R$ denotes the image under the canonical homomorphism $\mathbb{Z} \to R$.