Mathlib.Algebra.BigOperators.Ring.List

Commute.list_sum_right theorem

(a : R) (l : List R) (h : ∀ b ∈ l, Commute a b) : Commute a l.sum

Full source

lemma list_sum_right (a : R) (l : List R) (h : ∀ b ∈ l, Commute a b) : Commute a l.sum := by
  induction l with
  | nil => exact Commute.zero_right _
  | cons x xs ih =>
    rw [List.sum_cons]
    exact (h _ mem_cons_self).add_right (ih fun j hj ↦ h _ <| mem_cons_of_mem _ hj)

Commutation of an Element with the Sum of a Commuting List

Informal description

Let $R$ be a ring and let $a \in R$. For any list $l$ of elements in $R$, if $a$ commutes with every element $b \in l$ (i.e., $a * b = b * a$ for all $b \in l$), then $a$ commutes with the sum of the list $l$.

Commute.list_sum_left theorem

(b : R) (l : List R) (h : ∀ a ∈ l, Commute a b) : Commute l.sum b

Full source

lemma list_sum_left (b : R) (l : List R) (h : ∀ a ∈ l, Commute a b) : Commute l.sum b :=
  ((Commute.list_sum_right _ _) fun _x hx ↦ (h _ hx).symm).symm

Commutation of Sum of Commuting List with Element

Informal description

Let $R$ be a ring and let $b \in R$. For any list $l$ of elements in $R$, if every element $a \in l$ commutes with $b$ (i.e., $a * b = b * a$ for all $a \in l$), then the sum of the list $l$ commutes with $b$.

List.prod_map_neg theorem

(l : List M) : (l.map Neg.neg).prod = (-1) ^ l.length * l.prod

Full source

@[simp]
lemma prod_map_neg (l : List M) :
    (l.map Neg.neg).prod = (-1) ^ l.length * l.prod := by
  induction l <;> simp [*, pow_succ, ((Commute.neg_one_left _).pow_left _).left_comm]

Product of Negated List Equals $(-1)^{|l|}$ Times Original Product

Informal description

For any list $l$ of elements in a monoid $M$, the product of the list obtained by negating each element of $l$ is equal to $(-1)^{|l|}$ multiplied by the product of the original list $l$, i.e., $$\prod_{x \in l} (-x) = (-1)^{|l|} \cdot \prod_{x \in l} x.$$

List.prod_eq_zero theorem

 :
  ∀ {l : List M₀},
    (0 : M₀) ∈ l →
      l.prod =
        0
          -- |  absurd h (not_mem_nil _)

Full source

/-- 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`. -/
lemma prod_eq_zero : ∀ {l : List M₀}, (0 : M₀) ∈ l → l.prod = 0
  -- |  absurd h (not_mem_nil _)
  | a :: l, h => by
    rw [prod_cons]
    rcases mem_cons.1 h with ha | hl
    exacts [mul_eq_zero_of_left ha.symm _, mul_eq_zero_of_right _ (prod_eq_zero hl)]

Product of List Containing Zero is Zero

Informal description

For any list $l$ of elements in a monoid with zero $M₀$, if $0$ is an element of $l$, then the product of the elements in $l$ is equal to $0$, i.e., $\prod l = 0$.

List.prod_eq_zero_iff theorem

: ∀ {l : List M₀}, l.prod = 0 ↔ (0 : M₀) ∈ l

Full source

/-- 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. -/
@[simp] lemma prod_eq_zero_iff : ∀ {l : List M₀}, l.prod = 0 ↔ (0 : M₀) ∈ l
  | [] => by simp
  | a :: l => by rw [prod_cons, mul_eq_zero, prod_eq_zero_iff, mem_cons, eq_comm]

Product of List Equals Zero if and only if List Contains Zero

Informal description

For any list $l$ of elements in a monoid with zero $M₀$, the product of the elements in $l$ equals zero if and only if $0$ is an element of $l$, i.e., $\prod l = 0 \leftrightarrow 0 \in l$.

List.prod_ne_zero theorem

(hL : (0 : M₀) ∉ l) : l.prod ≠ 0

Full source

lemma prod_ne_zero (hL : (0 : M₀) ∉ l) : l.prod ≠ 0 := mt prod_eq_zero_iff.1 hL

Nonzero Product of List Without Zero

Informal description

For any list $l$ of elements in a monoid with zero $M₀$, if $0$ is not an element of $l$, then the product of the elements in $l$ is not equal to zero, i.e., $\prod l \neq 0$.

List.sum_map_mul_left theorem

: (l.map fun b ↦ r * f b).sum = r * (l.map f).sum

Full source

lemma sum_map_mul_left : (l.map fun b ↦ r * f b).sum = r * (l.map f).sum :=
  sum_map_hom l f <| AddMonoidHom.mulLeft r

Left Multiplicativity of Sum over List in Ring

Informal description

For any list $l$ of elements in a ring $R$, any element $r \in R$, and any function $f$ from the elements of $l$ to $R$, the sum of the list obtained by mapping each element $b \in l$ to $r \cdot f(b)$ is equal to $r$ multiplied by the sum of the list obtained by mapping $f$ over $l$. In other words, \[ \sum_{b \in l} (r \cdot f(b)) = r \cdot \left( \sum_{b \in l} f(b) \right). \]

List.sum_map_mul_right theorem

: (l.map fun b ↦ f b * r).sum = (l.map f).sum * r

Full source

lemma sum_map_mul_right : (l.map fun b ↦ f b * r).sum = (l.map f).sum * r :=
  sum_map_hom l f <| AddMonoidHom.mulRight r

Right Multiplicative Distributivity of Sum over List Mapping

Informal description

For any list $l$ of elements in a semiring $R$, any function $f$ mapping elements of $l$ to $R$, and any element $r \in R$, the sum of the list obtained by mapping each element $b \in l$ to $f(b) \cdot r$ is equal to the sum of the list obtained by mapping $f$ over $l$, multiplied by $r$. In other words: \[ \sum_{b \in l} f(b) \cdot r = \left(\sum_{b \in l} f(b)\right) \cdot r. \]

List.dvd_sum theorem

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

Full source

lemma dvd_sum [NonUnitalSemiring R] {a} {l : List R} (h : ∀ x ∈ l, a ∣ x) : a ∣ l.sum := by
  induction l with
  | nil => exact dvd_zero _
  | cons x l ih =>
    rw [List.sum_cons]
    exact dvd_add (h _ mem_cons_self) (ih fun x hx ↦ h x (mem_cons_of_mem _ hx))

Divisibility of Sum by Common Divisor in Non-Unital Semiring

Informal description

Let $R$ be a non-unital semiring, $a$ an element of $R$, and $l$ a list of elements of $R$. If $a$ divides every element $x$ in $l$, then $a$ divides the sum of all elements in $l$.

List.sum_zipWith_distrib_left theorem

 [NonUnitalNonAssocSemiring R] (f : ι → κ → R) (a : R) :
  ∀ (l₁ : List ι) (l₂ : List κ), (zipWith (fun i j ↦ a * f i j) l₁ l₂).sum = a * (zipWith f l₁ l₂).sum

Full source

@[simp] lemma sum_zipWith_distrib_left [NonUnitalNonAssocSemiring R] (f : ι → κ → R) (a : R) :
    ∀ (l₁ : List ι) (l₂ : List κ),
      (zipWith (fun i j ↦ a * f i j) l₁ l₂).sum = a * (zipWith f l₁ l₂).sum
  | [], _ => by simp
  | _, [] => by simp
  | i :: l₁, j :: l₂ => by simp [sum_zipWith_distrib_left, mul_add]

Left Distributivity of Scalar Multiplication over Zipped List Summation

Informal description

Let $R$ be a non-unital non-associative semiring, $f : \iota \times \kappa \to R$ be a function, and $a \in R$. For any lists $l_1$ of elements in $\iota$ and $l_2$ of elements in $\kappa$, the sum of the list obtained by applying $\lambda i\, j, a \cdot f(i,j)$ to corresponding elements of $l_1$ and $l_2$ equals $a$ multiplied by the sum of the list obtained by applying $f$ to corresponding elements of $l_1$ and $l_2$. In other words: \[ \sum_{(i,j) \in \text{zip}(l_1,l_2)} a \cdot f(i,j) = a \cdot \sum_{(i,j) \in \text{zip}(l_1,l_2)} f(i,j) \]