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

theorem Commute.list_sum_right {R : Type u_8} (a : R) (l : List R) (h : ∀ (b : R), b lCommute a b) :
Commute a ()
theorem Commute.list_sum_left {R : Type u_8} (b : R) (l : List R) (h : ∀ (a : R), a lCommute a b) :
Commute () b
theorem List.card_nsmul_le_sum {M : Type u_3} [] [] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x x_1] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x x_1] (l : List M) (n : M) (h : ∀ (x : M), x ln x) :
n
theorem List.pow_card_le_prod {M : Type u_3} [] [] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x x_1] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x x_1] (l : List M) (n : M) (h : ∀ (x : M), x ln x) :
n ^
theorem List.sum_eq_zero_iff {M : Type u_3} (l : List M) :
= 0 ∀ (x : M), x lx = 0
theorem List.prod_eq_one_iff {M : Type u_3} (l : List M) :
= 1 ∀ (x : M), x lx = 1
theorem List.neg_one_mem_of_prod_eq_neg_one {l : } (h : = -1) :
-1 l

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

theorem List.length_le_sum_of_one_le (L : ) (h : ∀ (i : ), i L1 i) :

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.

theorem List.dvd_prod {M : Type u_3} [] {a : M} {l : List M} (ha : a l) :
a
theorem List.dvd_sum {R : Type u_8} {a : R} {l : List R} (h : ∀ (x : R), x la x) :
a
theorem List.alternatingSum_append {α : Type u_2} [] (l₁ : List α) (l₂ : List α) :
List.alternatingSum (l₁ ++ l₂) = + (-1) ^
abbrev List.alternatingSum_append.match_1 {α : Type u_1} (motive : List αList αProp) :
∀ (x x_1 : List α), (∀ (l₂ : List α), motive [] l₂)(∀ (a : α) (l₁ l₂ : List α), motive (a :: l₁) l₂)motive x x_1
Equations
• (_ : motive x✝ x) = (_ : motive x✝ x)
Instances For
theorem List.alternatingProd_append {α : Type u_2} [] (l₁ : List α) (l₂ : List α) :
List.alternatingProd (l₁ ++ l₂) = * ^ (-1) ^
theorem List.alternatingSum_reverse {α : Type u_2} [] (l : List α) :
= (-1) ^ ( + 1)
abbrev List.alternatingSum_reverse.match_1 {α : Type u_1} (motive : List αProp) :
∀ (x : List α), (Unitmotive [])(∀ (a : α) (l : List α), motive (a :: l))motive x
Equations
• (_ : motive x) = (_ : motive x)
Instances For
theorem List.alternatingProd_reverse {α : Type u_2} [] (l : List α) :
= ^ (-1) ^ ( + 1)
theorem List.sum_map_mul_left {ι : Type u_1} {R : Type u_8} (L : List ι) (f : ιR) (r : R) :
List.sum (List.map (fun (b : ι) => r * f b) L) = r * List.sum (List.map f L)
theorem List.sum_map_mul_right {ι : Type u_1} {R : Type u_8} (L : List ι) (f : ιR) (r : R) :
List.sum (List.map (fun (b : ι) => f b * r) L) = List.sum (List.map f L) * r
theorem MulOpposite.op_list_prod {M : Type u_3} [] (l : List M) :
= List.prod (List.reverse (List.map MulOpposite.op l))
theorem MulOpposite.unop_list_prod {M : Type u_3} [] (l : ) :
= List.prod (List.reverse (List.map MulOpposite.unop l))
theorem unop_map_list_prod {M : Type u_3} {N : Type u_4} [] [] {F : Type u_9} [FunLike F M Nᵐᵒᵖ] [] (f : F) (l : List M) :
MulOpposite.unop (f ()) = List.prod (List.reverse (List.map (MulOpposite.unop f) l))

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

@[deprecated unop_map_list_prod]
theorem MonoidHom.unop_map_list_prod {M : Type u_3} {N : Type u_4} [] [] (f : M →* Nᵐᵒᵖ) (l : List M) :
MulOpposite.unop (f ()) = List.prod (List.reverse (List.map (MulOpposite.unop f) l))

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