theorem List.sum_pos_iff_exists_pos_nat {l : List Nat} : 0 < l.sum ↔ ∃ (x : Nat), x ∈ l ∧ 0 < x

@[deprecated List.sum_pos_iff_exists_pos_nat (since := "2025-01-15")]

def Nat.sum_pos_iff_exists_pos {l : List Nat} : 0 < l.sum ↔ ∃ (x : Nat), x ∈ l ∧ 0 < x

Equations

• @Nat.sum_pos_iff_exists_pos = @List.sum_pos_iff_exists_pos_nat

theorem List.sum_eq_zero_iff_forall_eq_nat {xs : List Nat} : xs.sum = 0 ↔ ∀ (x : Nat), x ∈ xs → x = 0

@[deprecated List.sum_pos_iff_exists_pos_nat (since := "2025-01-15")]

def Nat.sum_eq_zero_iff_forall_eq {xs : List Nat} : xs.sum = 0 ↔ ∀ (x : Nat), x ∈ xs → x = 0

Equations

• @Nat.sum_eq_zero_iff_forall_eq = @List.sum_eq_zero_iff_forall_eq_nat

@[simp]

theorem List.sum_replicate_nat {n a : Nat} : (replicate n a).sum = n * a

theorem List.sum_append_nat {l₁ l₂ : List Nat} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum

theorem List.sum_reverse_nat (xs : List Nat) : xs.reverse.sum = xs.sum

theorem List.sum_eq_foldl_nat {xs : List Nat} : xs.sum = foldl (fun (x1 x2 : Nat) => x1 + x2) 0 xs

theorem List.min_mul_length_le_sum_nat {xs : List Nat} (h : xs ≠ []) : xs.min h * xs.length ≤ xs.sum

theorem List.mul_length_le_sum_of_min?_eq_some_nat {x : Nat} {xs : List Nat} (h : xs.min? = some x) : x * xs.length ≤ xs.sum

theorem List.min_le_sum_div_length_nat {xs : List Nat} (h : xs ≠ []) : xs.min h ≤ xs.sum / xs.length

theorem List.le_sum_div_length_of_min?_eq_some_nat {x : Nat} {xs : List Nat} (h : xs.min? = some x) : x ≤ xs.sum / xs.length

theorem List.sum_le_max_mul_length_nat {xs : List Nat} (h : xs ≠ []) : xs.sum ≤ xs.max h * xs.length

theorem List.sum_le_max_mul_length_of_max?_eq_some_nat {x : Nat} {xs : List Nat} (h : xs.max? = some x) : xs.sum ≤ x * xs.length

theorem List.sum_div_length_le_max_nat {xs : List Nat} (h : xs ≠ []) : xs.sum / xs.length ≤ xs.max h

theorem List.sum_div_length_le_max_of_max?_eq_some_nat {x : Nat} {xs : List Nat} (h : xs.max? = some x) : xs.sum / xs.length ≤ x