Mathlib.Algebra.BigOperators.Group.List.Lemmas

List.prod_isUnit theorem

: ∀ {L : List M}, (∀ m ∈ L, IsUnit m) → IsUnit L.prod

Full source

@[to_additive]
theorem prod_isUnit : ∀ {L : List M}, (∀ m ∈ L, IsUnit m) → IsUnit L.prod
  | [], _ => by simp
  | h :: t, u => by
    simp only [List.prod_cons]
    exact IsUnit.mul (u h mem_cons_self) (prod_isUnit fun m mt => u m (mem_cons_of_mem h mt))

Product of Units in a List is a Unit

Informal description

For any list $L$ of elements in a monoid $M$, if every element $m$ in $L$ is a unit, then the product $\prod L$ is also a unit.

List.prod_isUnit_iff theorem

{α : Type*} [CommMonoid α] {L : List α} : IsUnit L.prod ↔ ∀ m ∈ L, IsUnit m

Full source

@[to_additive]
theorem prod_isUnit_iff {α : Type*} [CommMonoid α] {L : List α} :
    IsUnitIsUnit L.prod ↔ ∀ m ∈ L, IsUnit m := by
  refine ⟨fun h => ?_, prod_isUnit⟩
  induction L with
  | nil => exact fun m' h' => False.elim (not_mem_nil h')
  | cons m L ih =>
    rw [prod_cons, IsUnit.mul_iff] at h
    exact fun m' h' ↦ Or.elim (eq_or_mem_of_mem_cons h') (fun H => H.substr h.1) fun H => ih h.2 _ H

Product is Unit iff All Elements are Units in a Commutative Monoid

Informal description

Let $L$ be a list of elements in a commutative monoid $\alpha$. The product $\prod L$ is a unit if and only if every element $m$ in $L$ is a unit.

List.Perm.prod_eq' theorem

(h : l₁ ~ l₂) (hc : l₁.Pairwise Commute) : l₁.prod = l₂.prod

Full source

/-- If elements of a list commute with each other, then their product does not
depend on the order of elements. -/
@[to_additive "If elements of a list additively commute with each other, then their sum does not
depend on the order of elements."]
lemma Perm.prod_eq' (h : l₁ ~ l₂) (hc : l₁.Pairwise Commute) : l₁.prod = l₂.prod := by
  refine h.foldr_eq' ?_ _
  apply Pairwise.forall_of_forall
  · intro x y h z
    exact (h z).symm
  · intros; rfl
  · apply hc.imp
    intro a b h z
    rw [← mul_assoc, ← mul_assoc, h]

Product Invariance Under Permutation of Commuting Elements

Informal description

Let $l_1$ and $l_2$ be two lists of elements in a monoid $M$. If $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$) and the elements of $l_1$ pairwise commute (i.e., for any two distinct elements $x, y \in l_1$, $x * y = y * x$), then the product of the elements in $l_1$ equals the product of the elements in $l_2$, i.e., $\prod l_1 = \prod l_2$.

List.prod_rotate_eq_one_of_prod_eq_one theorem

: ∀ {l : List G} (_ : l.prod = 1) (n : ℕ), (l.rotate n).prod = 1

Full source

lemma prod_rotate_eq_one_of_prod_eq_one :
    ∀ {l : List G} (_ : l.prod = 1) (n : ℕ), (l.rotate n).prod = 1
  | [], _, _ => by simp
  | a :: l, hl, n => by
    have : n % List.length (a :: l) ≤ List.length (a :: l) := le_of_lt (Nat.mod_lt _ (by simp))
    rw [← List.take_append_drop (n % List.length (a :: l)) (a :: l)] at hl
    rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq,
      ← one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_cancel, mul_one]

Rotation Invariance of Product Identity in Groups: $\prod l = 1 \implies \prod (l.\text{rotate}\, n) = 1$

Informal description

For any list $l$ of elements in a group $G$ such that the product of all elements in $l$ is the identity element $1$, and for any natural number $n$, the product of the elements in the list obtained by rotating $l$ by $n$ positions is also equal to $1$.

List.sum_map_count_dedup_filter_eq_countP theorem

(p : α → Bool) (l : List α) : ((l.dedup.filter p).map fun x => l.count x).sum = l.countP p

Full source

/-- Summing the count of `x` over a list filtered by some `p` is just `countP` applied to `p` -/
theorem sum_map_count_dedup_filter_eq_countP (p : α → Bool) (l : List α) :
    ((l.dedup.filter p).map fun x => l.count x).sum = l.countP p := by
  induction l with
  | nil => simp
  | cons a as h =>
    simp_rw [List.countP_cons, List.count_cons, List.sum_map_add]
    congr 1
    · refine _root_.trans ?_ h
      by_cases ha : a ∈ as
      · simp [dedup_cons_of_mem ha]
      · simp only [dedup_cons_of_not_mem ha, List.filter]
        match p a with
        | true => simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
        | false => simp only
    · simp only [beq_iff_eq]
      by_cases hp : p a
      · refine _root_.trans (sum_map_eq_nsmul_single a _ fun _ h _ => by simp [h.symm]) ?_
        simp [hp, count_dedup]
      · refine _root_.trans (List.sum_eq_zero fun n hn => ?_) (by simp [hp])
        obtain ⟨a', ha'⟩ := List.mem_map.1 hn
        split_ifs at ha' with ha
        · simp only [ha.symm, mem_filter, mem_dedup, find?, mem_cons, true_or, hp,
            and_false, false_and, reduceCtorEq] at ha'
        · exact ha'.2.symm

Sum of Counts in Filtered Deduplicated List Equals Count of Predicate

Informal description

For any predicate $p$ on elements of type $\alpha$ and any list $l$ of elements of type $\alpha$, the sum of the counts of each element in the filtered deduplicated list equals the count of elements in $l$ that satisfy $p$. In symbols: $$\sum_{x \in \mathrm{dedup}(l) \text{ and } p(x)} \mathrm{count}(x, l) = \mathrm{countP}(p, l)$$

List.sum_map_count_dedup_eq_length theorem

(l : List α) : (l.dedup.map fun x => l.count x).sum = l.length

Full source

theorem sum_map_count_dedup_eq_length (l : List α) :
    (l.dedup.map fun x => l.count x).sum = l.length := by
  simpa using sum_map_count_dedup_filter_eq_countP (fun _ => True) l

Sum of Element Counts in Deduplicated List Equals Original Length

Informal description

For any list $l$ of elements of type $\alpha$, the sum of the counts of each element in the deduplicated version of $l$ equals the length of $l$. In symbols: $$\sum_{x \in \mathrm{dedup}(l)} \mathrm{count}(x, l) = \mathrm{length}(l)$$

List.length_sigma theorem

 {σ : α → Type*} (l₁ : List α) (l₂ : ∀ a, List (σ a)) : length (l₁.sigma l₂) = (l₁.map fun a ↦ length (l₂ a)).sum

Full source

lemma length_sigma {σ : α → Type*} (l₁ : List α) (l₂ : ∀ a, List (σ a)) :
    length (l₁.sigma l₂) = (l₁.map fun a ↦ length (l₂ a)).sum := by
  induction' l₁ with x l₁ IH
  · rfl
  · simp only [sigma_cons, length_append, length_map, IH, map, sum_cons]

Length of Dependent Product List Equals Sum of Component Lengths

Informal description

For any type family $\sigma : \alpha \to \text{Type}$ and lists $l_1 : \text{List } \alpha$, $l_2 : \forall a, \text{List } (\sigma a)$, the length of the dependent product list $l_1.\text{sigma } l_2$ is equal to the sum of the lengths of the lists $l_2(a)$ for each $a$ in $l_1$. In symbols: $$\text{length}(l_1.\text{sigma } l_2) = \sum_{a \in l_1} \text{length}(l_2(a))$$

List.ranges_flatten theorem

: ∀ (l : List ℕ), l.ranges.flatten = range l.sum

Full source

lemma ranges_flatten : ∀ (l : List ℕ), l.ranges.flatten = range l.sum
  | [] => rfl
  | a :: l => by simp [ranges, ← map_flatten, ranges_flatten, range_add]

Concatenation of Ranges Equals Range of Sum

Informal description

For any list of natural numbers $l$, the concatenation of all sublists in `l.ranges` is equal to the list `[0, 1, ..., (l.sum) - 1]`.

List.ranges_nodup theorem

{l s : List ℕ} (hs : s ∈ ranges l) : s.Nodup

Full source

/-- The members of `l.ranges` have no duplicate -/
theorem ranges_nodup {l s : List ℕ} (hs : s ∈ ranges l) : s.Nodup :=
  (List.pairwise_flatten.mp <| by rw [ranges_flatten]; exact nodup_range).1 s hs

No Duplicates in Sublists of Ranges

Informal description

For any list of natural numbers $l$ and any sublist $s$ in the ranges of $l$ (i.e., $s \in \text{ranges}(l)$), the sublist $s$ has no duplicate elements.

List.mem_mem_ranges_iff_lt_sum theorem

(l : List ℕ) {n : ℕ} : (∃ s ∈ l.ranges, n ∈ s) ↔ n < l.sum

Full source

/-- Any entry of any member of `l.ranges` is strictly smaller than `l.sum`. -/
lemma mem_mem_ranges_iff_lt_sum (l : List ℕ) {n : ℕ} :
    (∃ s ∈ l.ranges, n ∈ s) ↔ n < l.sum := by
  rw [← mem_range, ← ranges_flatten, mem_flatten]

Membership in Sublists of Ranges is Equivalent to Being Less Than Sum of List Elements

Informal description

For any list of natural numbers $l$ and any natural number $n$, there exists a sublist $s$ in the ranges of $l$ (i.e., $s \in \text{ranges}(l)$) such that $n \in s$ if and only if $n$ is strictly less than the sum of all elements in $l$.

List.drop_take_succ_flatten_eq_getElem theorem

 (L : List (List α)) (i : Nat) (h : i < L.length) :
  (L.flatten.take ((L.map length).take (i + 1)).sum).drop ((L.map length).take i).sum = L[i]

Full source

/-- In a flatten of sublists, taking the slice between the indices `A` and `B - 1` gives back the
original sublist of index `i` if `A` is the sum of the lengths of sublists of index `< i`, and
`B` is the sum of the lengths of sublists of index `≤ i`. -/
lemma drop_take_succ_flatten_eq_getElem (L : List (List α)) (i : Nat) (h : i < L.length) :
    (L.flatten.take ((L.map length).take (i + 1)).sum).drop ((L.map length).take i).sum = L[i] := by
  have : (L.map length).take i = ((L.take (i + 1)).map length).take i := by
    simp [map_take, take_take, Nat.min_eq_left]
  simp only [this, length_map, take_sum_flatten, drop_sum_flatten,
    drop_take_succ_eq_cons_getElem, h, flatten, append_nil]

Extracting Sublist from Flattened List via Cumulative Lengths

Informal description

For any list of lists $L$ of elements of type $\alpha$ and any natural number $i$ such that $i < \text{length}(L)$, the operation of flattening $L$, taking the first $\sum_{j=0}^i \text{length}(L[j])$ elements, and then dropping the first $\sum_{j=0}^{i-1} \text{length}(L[j])$ elements results in the $i$-th sublist of $L$. That is, \[ \text{drop}\ \left(\sum_{j=0}^{i-1} \text{length}(L[j])\right)\ \left(\text{take}\ \left(\sum_{j=0}^i \text{length}(L[j])\right)\ L.\text{flatten}\right) = L[i]. \]

List.neg_one_mem_of_prod_eq_neg_one theorem

{l : List ℤ} (h : l.prod = -1) : (-1 : ℤ) ∈ l

Full source

/-- If a product of integers is `-1`, then at least one factor must be `-1`. -/
theorem neg_one_mem_of_prod_eq_neg_one {l : List ℤ} (h : l.prod = -1) : (-1 : ℤ) ∈ l := by
  obtain ⟨x, h₁, h₂⟩ := exists_mem_ne_one_of_prod_ne_one (ne_of_eq_of_ne h (by decide))
  exact Or.resolve_left
    (Int.isUnit_iff.mp (prod_isUnit_iff.mp
      (h.symm ▸ ⟨⟨-1, -1, by decide, by decide⟩, rfl⟩ : IsUnit l.prod) x h₁)) h₂ ▸ h₁

Presence of $-1$ in Integer List with Product $-1$

Informal description

For any list of integers $l$, if the product of all elements in $l$ is $-1$, then $-1$ is an element of $l$.

List.dvd_prod theorem

[CommMonoid M] {a} {l : List M} (ha : a ∈ l) : a ∣ l.prod

Full source

theorem dvd_prod [CommMonoid M] {a} {l : List M} (ha : a ∈ l) : a ∣ l.prod := by
  let ⟨s, t, h⟩ := append_of_mem ha
  rw [h, prod_append, prod_cons, mul_left_comm]
  exact dvd_mul_right _ _

Element of List Divides Product in Commutative Monoid

Informal description

Let $M$ be a commutative monoid. For any element $a \in M$ and any list $l$ of elements of $M$, if $a$ is an element of $l$, then $a$ divides the product of all elements in $l$, i.e., $a \mid \prod_{x \in l} x$.

List.Sublist.prod_dvd_prod theorem

[CommMonoid M] {l₁ l₂ : List M} (h : l₁ <+ l₂) : l₁.prod ∣ l₂.prod

Full source

theorem Sublist.prod_dvd_prod [CommMonoid M] {l₁ l₂ : List M} (h : l₁ <+ l₂) :
    l₁.prod ∣ l₂.prod := by
  obtain ⟨l, hl⟩ := h.exists_perm_append
  rw [hl.prod_eq, prod_append]
  exact dvd_mul_right _ _

Sublist Product Divisibility in Commutative Monoid

Informal description

Let $M$ be a commutative monoid and let $l_1, l_2$ be lists of elements of $M$. If $l_1$ is a sublist of $l_2$, then the product of elements in $l_1$ divides the product of elements in $l_2$, i.e., $\prod_{x \in l_1} x \mid \prod_{y \in l_2} y$.

List.alternatingProd_append theorem

 : ∀ l₁ l₂ : List α, alternatingProd (l₁ ++ l₂) = alternatingProd l₁ * alternatingProd l₂ ^ (-1 : ℤ) ^ length l₁

Full source

@[to_additive]
theorem alternatingProd_append :
    ∀ l₁ l₂ : List α,
      alternatingProd (l₁ ++ l₂) = alternatingProd l₁ * alternatingProd l₂ ^ (-1 : ℤ) ^ length l₁
  | [], l₂ => by simp
  | a :: l₁, l₂ => by
    simp_rw [cons_append, alternatingProd_cons, alternatingProd_append, length_cons, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, ← div_eq_mul_inv, div_div]

Alternating Product of Concatenated Lists: $\text{alternatingProd}(l_1 ++ l_2) = \text{alternatingProd}(l_1) \cdot \text{alternatingProd}(l_2)^{(-1)^{|l_1|}}$

Informal description

Let $\alpha$ be a commutative group. For any two lists $l_1$ and $l_2$ of elements of $\alpha$, the alternating product of their concatenation $l_1 ++ l_2$ is given by: $$\text{alternatingProd}(l_1 ++ l_2) = \text{alternatingProd}(l_1) \cdot \text{alternatingProd}(l_2)^{(-1)^{|l_1|}}$$ where $\text{alternatingProd}(l)$ denotes the alternating product of the list $l$ (i.e., $a_1 \cdot a_2^{-1} \cdot a_3 \cdot a_4^{-1} \cdots$ for $l = [a_1, a_2, a_3, a_4, \dots]$), and $|l_1|$ is the length of $l_1$.

List.alternatingProd_reverse theorem

: ∀ l : List α, alternatingProd (reverse l) = alternatingProd l ^ (-1 : ℤ) ^ (length l + 1)

Full source

@[to_additive]
theorem alternatingProd_reverse :
    ∀ l : List α, alternatingProd (reverse l) = alternatingProd l ^ (-1 : ℤ) ^ (length l + 1)
  | [] => by simp only [alternatingProd_nil, one_zpow, reverse_nil]
  | a :: l => by
    simp_rw [reverse_cons, alternatingProd_append, alternatingProd_reverse,
      alternatingProd_singleton, alternatingProd_cons, length_reverse, length, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, inv_inv]
    rw [mul_comm, ← div_eq_mul_inv, div_zpow]

Alternating Product of Reversed List: $\text{alternatingProd}(\text{reverse}(l)) = \text{alternatingProd}(l)^{(-1)^{|l| + 1}}$

Informal description

Let $\alpha$ be a commutative group. For any list $l$ of elements of $\alpha$, the alternating product of the reversed list equals the alternating product of $l$ raised to the power $(-1)^{|l| + 1}$, where $|l|$ is the length of $l$. That is, $$\text{alternatingProd}(\text{reverse}(l)) = \text{alternatingProd}(l)^{(-1)^{|l| + 1}}$$ where $\text{alternatingProd}(l)$ denotes the alternating product of the list $l$ (i.e., $a_1 \cdot a_2^{-1} \cdot a_3 \cdot a_4^{-1} \cdots$ for $l = [a_1, a_2, a_3, a_4, \dots]$).

MulOpposite.op_list_prod theorem

: ∀ l : List M, op l.prod = (l.map op).reverse.prod

Full source

lemma op_list_prod : ∀ l : List M, op l.prod = (l.map op).reverse.prod := by
  intro l; induction l with
  | nil => rfl
  | cons x xs ih =>
    rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]

Product Reversal in Multiplicative Opposite: $\text{op}(\prod l) = \prod (\text{reverse}(\text{map op } l))$

Informal description

For any list $l$ of elements in a monoid $M$, the multiplicative opposite of the product of $l$ is equal to the product of the reversed list obtained by mapping each element of $l$ to its multiplicative opposite. In symbols: $$\text{op}\left(\prod_{x \in l} x\right) = \prod_{x \in \text{reverse}(\text{map op } l)} x$$

MulOpposite.unop_list_prod theorem

(l : List Mᵐᵒᵖ) : l.prod.unop = (l.map unop).reverse.prod

Full source

lemma unop_list_prod (l : List Mᵐᵒᵖ) : l.prod.unop = (l.map unop).reverse.prod := by
  rw [← op_inj, op_unop, MulOpposite.op_list_prod, map_reverse, map_map, reverse_reverse,
    op_comp_unop, map_id]

Projection of Product in Multiplicative Opposite Equals Reversed Product of Projections

Informal description

For any list $l$ of elements in the multiplicative opposite $M^\text{op}$ of a monoid $M$, the projection of the product of $l$ back to $M$ is equal to the product of the reversed list obtained by projecting each element of $l$ back to $M$. In symbols: $$\text{unop}\left(\prod_{x \in l} x\right) = \prod_{x \in \text{reverse}(\text{map unop } l)} x$$

unop_map_list_prod theorem

 {F : Type*} [FunLike F M Nᵐᵒᵖ] [MonoidHomClass F M Nᵐᵒᵖ] (f : F) (l : List M) :
  (f l.prod).unop = (l.map (MulOpposite.unop ∘ f)).reverse.prod

Full source

/-- A morphism into the opposite monoid acts on the product by acting on the reversed elements. -/
lemma unop_map_list_prod {F : Type*} [FunLike F M Nᵐᵒᵖ] [MonoidHomClass F M Nᵐᵒᵖ]
    (f : F) (l : List M) :
    (f l.prod).unop = (l.map (MulOpposite.unopMulOpposite.unop ∘ f)).reverse.prod := by
  rw [map_list_prod f l, MulOpposite.unop_list_prod, List.map_map]

Projection of Homomorphic Product in Opposite Monoid Equals Reversed Product of Projected Homomorphisms

Informal description

Let $M$ and $N$ be monoids, and let $F$ be a type of homomorphisms from $M$ to the multiplicative opposite $N^\text{op}$ of $N$ that preserve the monoid structure. For any homomorphism $f \in F$ and any list $l$ of elements in $M$, the projection of $f$ applied to the product of $l$ back to $N$ equals the product of the reversed list obtained by composing the projection with $f$ on each element of $l$. In symbols: $$(f(\prod_{x \in l} x)).\text{unop} = \prod_{x \in \text{reverse}(\text{map } (\text{unop} \circ f) \ l)} x$$