Sums and products from lists #
This file provides basic results about list.prod
, list.sum
, which calculate the product and sum
of elements of a list and list.alternating_prod
, list.alternating_sum
, their alternating
counterparts. These are defined in data.list.defs
.
A list with sum not zero must have positive length.
A list with positive sum must have positive length.
A list with negative sum must have positive length.
We'd like to state this as L.head + L.tail.sum = L.sum
, but because L.head
relies on an inhabited instance to return a garbage value on the empty list, this is not possible.
Instead, we write the statement in terms of (L.nth 0).get_or_else 0
.
We'd like to state this as L.head * L.tail.prod = L.prod
, but because L.head
relies on an
inhabited instance to return a garbage value on the empty list, this is not possible.
Instead, we write the statement in terms of (L.nth 0).get_or_else 1
.
If l₁
is a sublist of l₂
and all elements of l₂
are nonnegative,
then l₁.sum ≤ l₂.sum
. One can prove a stronger version assuming ∀ a ∈ l₂.diff l₁, 0 ≤ a
instead
of ∀ a ∈ l₂, 0 ≤ a
but this lemma is not yet in mathlib
.
If l₁
is a sublist of l₂
and all elements of l₂
are greater than or equal to one, then
l₁.prod ≤ l₂.prod
. One can prove a stronger version assuming ∀ a ∈ l₂.diff l₁, 1 ≤ a
instead
of ∀ a ∈ l₂, 1 ≤ a
but this lemma is not yet in mathlib
.
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
.
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.
Alternative version of list.prod_update_nth
when the list is over a group
Slightly more general version of list.sum_eq_zero_iff
for a non-ordered add_monoid
Slightly more general version of list.prod_eq_one_iff
for a non-ordered monoid
The product of a list of positive natural numbers is positive, and likewise for any nontrivial ordered semiring.
Several lemmas about sum/head/tail for list ℕ
.
These are hard to generalize well, as they rely on the fact that default ℕ = 0
.
If desired, we could add a class stating that default = 0
.
A morphism into the opposite monoid acts on the product by acting on the reversed elements.
Deprecated, use _root_.map_list_sum
instead.
A morphism into the opposite monoid acts on the product by acting on the reversed elements.
Deprecated, use _root_.unop_map_list_prod
instead.