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

ink

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

ink

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

ink

theorem List.card_nsmul_le_sum {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (l : List M) (n : M) (h : ∀ (x : M), x ∈ l → n ≤ x) : List.length l • n ≤ List.sum l

ink

theorem List.pow_card_le_prod {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (l : List M) (n : M) (h : ∀ (x : M), x ∈ l → n ≤ x) : n ^ List.length l ≤ List.prod l

ink

theorem List.sum_eq_zero_iff {M : Type u_1} [inst : CanonicallyOrderedAddMonoid M] (l : List M) : List.sum l = 0 ↔ ∀ (x : M), x ∈ l → x = 0

ink

theorem List.prod_eq_one_iff {M : Type u_1} [inst : CanonicallyOrderedMonoid M] (l : List M) : List.prod l = 1 ↔ ∀ (x : M), x ∈ l → x = 1

ink

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.

ink

theorem List.length_le_sum_of_one_le (L : List ℕ) (h : ∀ (i : ℕ), 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.

ink

theorem List.dvd_prod {M : Type u_1} [inst : CommMonoid M] {a : M} {l : List M} (ha : a ∈ l) : a ∣ List.prod l

ink

theorem List.dvd_sum {R : Type u_1} [inst : Semiring R] {a : R} {l : List R} (h : ∀ (x : R), x ∈ l → a ∣ x) : a ∣ List.sum l

ink

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

• List.alternatingSum_append.match_1 motive x x h_1 h_2 = List.casesOn x (h_1 x) fun head tail => h_2 head tail x

ink

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

ink

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

ink

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

ink

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

• List.alternatingSum_reverse.match_1 motive x h_1 h_2 = List.casesOn x (h_1 ()) fun head tail => h_2 head tail

ink

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

ink

theorem List.sum_map_mul_left {ι : Type u_2} {R : Type u_1} [inst : 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)

ink

theorem List.sum_map_mul_right {ι : Type u_2} {R : Type u_1} [inst : 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

ink

theorem MulOpposite.op_list_prod {M : Type u_1} [inst : Monoid M] (l : List M) : { unop := List.prod l } = List.prod (List.reverse (List.map MulOpposite.op l))

ink

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

ink

theorem unop_map_list_prod {M : Type u_2} {N : Type u_3} [inst : Monoid M] [inst : Monoid N] {F : Type u_1} [inst : MonoidHomClass F M Nᵐᵒᵖ] (f : F) (l : List M) : (↑f (List.prod l)).unop = 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.

ink

theorem MonoidHom.unop_map_list_prod {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Monoid N] (f : M →* Nᵐᵒᵖ) (l : List M) : (↑f (List.prod l)).unop = 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.