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

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

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

theorem List.neg_one_mem_of_prod_eq_neg_one {l : List ℤ} (h : List.prod l = -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 : List ℕ) (h : ∀ i ∈ L, 1 ≤ i) : List.length L ≤ List.sum L

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} [CommMonoid M] {a : M} {l : List M} (ha : a ∈ l) : a ∣ List.prod l

theorem List.Sublist.prod_dvd_prod {M : Type u_3} [CommMonoid M] {l₁ : List M} {l₂ : List M} (h : List.Sublist l₁ l₂) : List.prod l₁ ∣ List.prod l₂

theorem List.prod_eq_zero {M₀ : Type u_6} [MonoidWithZero M₀] {L : List M₀} (h : 0 ∈ L) : List.prod L = 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_6} [MonoidWithZero M₀] [Nontrivial M₀] [NoZeroDivisors M₀] {L : List M₀} : List.prod L = 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_6} [MonoidWithZero M₀] [Nontrivial M₀] [NoZeroDivisors M₀] {L : List M₀} (hL : 0 ∉ L) : List.prod L ≠ 0

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

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

• ⋯ = ⋯

theorem List.alternatingSum_append {α : Type u_2} [AddCommGroup α] (l₁ : List α) (l₂ : List α) : List.alternatingSum (l₁ ++ l₂) = List.alternatingSum l₁ + (-1) ^ List.length l₁ • List.alternatingSum l₂

theorem List.alternatingProd_append {α : Type u_2} [CommGroup α] (l₁ : List α) (l₂ : List α) : List.alternatingProd (l₁ ++ l₂) = List.alternatingProd l₁ * List.alternatingProd l₂ ^ (-1) ^ List.length l₁

abbrev List.alternatingSum_reverse.match_1 {α : Type u_1} (motive : List α → Prop) : ∀ (x : List α), (Unit → motive []) → (∀ (a : α) (l : List α), motive (a :: l)) → motive x

Equations

• ⋯ = ⋯

theorem List.alternatingSum_reverse {α : Type u_2} [AddCommGroup α] (l : List α) : List.alternatingSum (List.reverse l) = (-1) ^ (List.length l + 1) • List.alternatingSum l

theorem List.alternatingProd_reverse {α : Type u_2} [CommGroup α] (l : List α) : List.alternatingProd (List.reverse l) = List.alternatingProd l ^ (-1) ^ (List.length l + 1)

theorem List.sum_map_mul_left {ι : Type u_1} {R : Type u_8} [NonUnitalNonAssocSemiring R] (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} [NonUnitalNonAssocSemiring R] (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} [Monoid M] (l : List M) : MulOpposite.op (List.prod l) = List.prod (List.reverse (List.map MulOpposite.op l))

theorem MulOpposite.unop_list_prod {M : Type u_3} [Monoid M] (l : List Mᵐᵒᵖ) : MulOpposite.unop (List.prod l) = List.prod (List.reverse (List.map MulOpposite.unop l))

theorem unop_map_list_prod {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] {F : Type u_9} [FunLike F M Nᵐᵒᵖ] [MonoidHomClass F M Nᵐᵒᵖ] (f : F) (l : List M) : MulOpposite.unop (f (List.prod l)) = 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} [Monoid M] [Monoid N] (f : M →* Nᵐᵒᵖ) (l : List M) : MulOpposite.unop (f (List.prod l)) = 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.