theorem
Commute.list_sum_right
{R : Type u_8}
[NonUnitalNonAssocSemiring R]
(a : R)
(l : List R)
(h : ∀ b ∈ l, Commute a b)
:
Commute a l.sum
theorem
Commute.list_sum_left
{R : Type u_8}
[NonUnitalNonAssocSemiring R]
(b : R)
(l : List R)
(h : ∀ a ∈ l, Commute a b)
:
Commute l.sum b
theorem
List.Sublist.prod_dvd_prod
{M : Type u_3}
[CommMonoid M]
{l₁ : List M}
{l₂ : List M}
(h : l₁.Sublist l₂)
:
l₁.prod ∣ l₂.prod
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₀}
:
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)
:
L.prod ≠ 0
theorem
List.dvd_sum
{R : Type u_8}
[NonUnitalSemiring R]
{a : R}
{l : List R}
(h : ∀ x ∈ l, a ∣ x)
:
a ∣ l.sum
theorem
MulOpposite.op_list_prod
{M : Type u_3}
[Monoid M]
(l : List M)
:
MulOpposite.op l.prod = (List.map MulOpposite.op l).reverse.prod