Big operators on a list in rings

This file contains the results concerning the interaction of list big operators with rings.

theorem Commute.list_sum_right {R : Type u_5} [NonUnitalNonAssocSemiring R] (a : R) (l : List R) (h : ∀ b ∈ l, Commute a b) : Commute a l.sum

theorem Commute.list_sum_left {R : Type u_5} [NonUnitalNonAssocSemiring R] (b : R) (l : List R) (h : ∀ a ∈ l, Commute a b) : Commute l.sum b

@[simp]

theorem List.prod_map_neg {M : Type u_3} [CommMonoid M] [HasDistribNeg M] (l : List M) : (List.map Neg.neg l).prod = (-1) ^ l.length * l.prod

theorem List.prod_eq_zero {M₀ : Type u_4} [MonoidWithZero M₀] {l : List M₀} : 0 ∈ l → l.prod = 0

If zero is an element of a list l, then List.prod l = 0. If the domain is a nontrivial monoid with zero with no divisors, then this implication becomes an iff, see List.prod_eq_zero_iff.

@[simp]

theorem List.prod_eq_zero_iff {M₀ : Type u_4} [MonoidWithZero M₀] [Nontrivial M₀] [NoZeroDivisors M₀] {l : List M₀} : l.prod = 0 ↔ 0 ∈ l

Product of elements of a list l equals zero if and only if 0 ∈ l. See also List.prod_eq_zero for an implication that needs weaker typeclass assumptions.

theorem List.prod_ne_zero {M₀ : Type u_4} [MonoidWithZero M₀] {l : List M₀} [Nontrivial M₀] [NoZeroDivisors M₀] (hL : 0 ∉ l) : l.prod ≠ 0

theorem List.sum_map_mul_left {ι : Type u_1} {R : Type u_5} [NonUnitalNonAssocSemiring R] (l : List ι) (f : ι → R) (r : R) : (List.map (fun (b : ι) => r * f b) l).sum = r * (List.map f l).sum

theorem List.sum_map_mul_right {ι : Type u_1} {R : Type u_5} [NonUnitalNonAssocSemiring R] (l : List ι) (f : ι → R) (r : R) : (List.map (fun (b : ι) => f b * r) l).sum = (List.map f l).sum * r

theorem List.dvd_sum {R : Type u_5} [NonUnitalSemiring R] {a : R} {l : List R} (h : ∀ x ∈ l, a ∣ x) : a ∣ l.sum

@[simp]

theorem List.sum_zipWith_distrib_left {ι : Type u_1} {κ : Type u_2} {R : Type u_5} [Semiring R] (f : ι → κ → R) (a : R) (l₁ : List ι) (l₂ : List κ) : (List.zipWith (fun (i : ι) (j : κ) => a * f i j) l₁ l₂).sum = a * (List.zipWith f l₁ l₂).sum