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)
:
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)
:
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
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
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
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₂
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₁
theorem
List.alternatingSum_reverse
{α : Type u_1}
[inst : AddCommGroup α]
(l : List α)
:
List.alternatingSum (List.reverse l) = (-1) ^ (List.length l + 1) • List.alternatingSum l
Equations
- List.alternatingSum_reverse.match_1 motive x h_1 h_2 = List.casesOn x (h_1 ()) fun head tail => h_2 head tail
theorem
List.alternatingProd_reverse
{α : Type u_1}
[inst : CommGroup α]
(l : List α)
:
List.alternatingProd (List.reverse l) = List.alternatingProd l ^ (-1) ^ (List.length l + 1)
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)
:
A morphism into the opposite monoid acts on the product by acting on the reversed elements.