mathlib3 documentation

data.list.big_operators.lemmas

Lemmas about list.sum and list.prod requiring extra algebra imports #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
theorem commute.list_sum_right {R : Type u_8} [non_unital_non_assoc_semiring R] (a : R) (l : list R) (h : ∀ (b : R), b ∈ l → commute a b) :
commute a l.sum
source
theorem commute.list_sum_left {R : Type u_8} [non_unital_non_assoc_semiring R] (b : R) (l : list R) (h : ∀ (a : R), a ∈ l → commute a b) :
commute l.sum b
source
theorem list.pow_card_le_prod {M : Type u_3} [monoid M] [preorder M] [covariant_class M M (function.swap has_mul.mul) has_le.le] [covariant_class M M has_mul.mul has_le.le] (l : list M) (n : M) (h : ∀ (x : M), x ∈ l → n ≤ x) :
n ^ l.length ≤ l.prod
source
theorem list.card_nsmul_le_sum {M : Type u_3} [add_monoid M] [preorder M] [covariant_class M M (function.swap has_add.add) has_le.le] [covariant_class M M has_add.add has_le.le] (l : list M) (n : M) (h : ∀ (x : M), x ∈ l → n ≤ x) :
l.length • n ≤ l.sum
source
theorem list.sum_eq_zero_iff {M : Type u_3} [canonically_ordered_add_monoid M] (l : list M) :
l.sum = 0 ↔ ∀ (x : M), x ∈ l → x = 0
source
theorem list.prod_eq_one_iff {M : Type u_3} [canonically_ordered_monoid M] (l : list M) :
l.prod = 1 ↔ ∀ (x : M), x ∈ l → x = 1
source
theorem list.neg_one_mem_of_prod_eq_neg_one {l : list ℤ} (h : l.prod = -1) :
-1 ∈ l

If a product of integers is -1, then at least one factor must be -1.

source
theorem list.length_le_sum_of_one_le (L : list ℕ) (h : ∀ (i : ℕ), i ∈ L → 1 ≤ i) :
L.length ≤ L.sum

If all elements in a list are bounded below by 1, then the length of the list is bounded by the sum of the elements.

source
theorem list.dvd_prod {M : Type u_3} [comm_monoid M] {a : M} {l : list M} (ha : a ∈ l) :
a ∣ l.prod
source
theorem list.dvd_sum {R : Type u_8} [semiring R] {a : R} {l : list R} (h : ∀ (x : R), x ∈ l → a ∣ x) :
a ∣ l.sum
source
theorem list.alternating_prod_append {α : Type u_2} [comm_group α] (l₁ l₂ : list α) :
(l₁ ++ l₂).alternating_prod = l₁.alternating_prod * l₂.alternating_prod ^ (-1) ^ l₁.length
source
theorem list.alternating_sum_append {α : Type u_2} [add_comm_group α] (l₁ l₂ : list α) :
(l₁ ++ l₂).alternating_sum = l₁.alternating_sum + (-1) ^ l₁.length • l₂.alternating_sum
source
theorem list.alternating_prod_reverse {α : Type u_2} [comm_group α] (l : list α) :
l.reverse.alternating_prod = l.alternating_prod ^ (-1) ^ (l.length + 1)
source
theorem list.alternating_sum_reverse {α : Type u_2} [add_comm_group α] (l : list α) :
l.reverse.alternating_sum = (-1) ^ (l.length + 1) • l.alternating_sum
source
theorem list.sum_map_mul_left {ι : Type u_1} {R : Type u_8} [non_unital_non_assoc_semiring R] (L : list ι) (f : ι → R) (r : R) :
(list.map (λ (b : ι), r * f b) L).sum = r * (list.map f L).sum
source
theorem list.sum_map_mul_right {ι : Type u_1} {R : Type u_8} [non_unital_non_assoc_semiring R] (L : list ι) (f : ι → R) (r : R) :
(list.map (λ (b : ι), f b * r) L).sum = (list.map f L).sum * r
source
theorem mul_opposite.op_list_prod {M : Type u_3} [monoid M] (l : list M) :
mul_opposite.op l.prod = (list.map mul_opposite.op l).reverse.prod
source
theorem mul_opposite.unop_list_prod {M : Type u_3} [monoid M] (l : list Mᵐᵒᵖ) :
mul_opposite.unop l.prod = (list.map mul_opposite.unop l).reverse.prod
source
theorem unop_map_list_prod {M : Type u_3} {N : Type u_4} [monoid M] [monoid N] {F : Type u_1} [monoid_hom_class F M Nᵐᵒᵖ] (f : F) (l : list M) :
mul_opposite.unop (⇑f l.prod) = (list.map (mul_opposite.unop ∘ ⇑f) l).reverse.prod

A morphism into the opposite monoid acts on the product by acting on the reversed elements.

source
@[protected]
theorem monoid_hom.unop_map_list_prod {M : Type u_3} {N : Type u_4} [monoid M] [monoid N] (f : M →* Nᵐᵒᵖ) (l : list M) :
mul_opposite.unop (⇑f l.prod) = (list.map (mul_opposite.unop ∘ ⇑f) l).reverse.prod

A morphism into the opposite monoid acts on the product by acting on the reversed elements.

Deprecated, use _root_.unop_map_list_prod instead.