Documentation

Mathlib.Algebra.BigOperators.WithTop

Sums in WithTop #

This file proves results about finite sums over monoids extended by a bottom or top element.

@[simp]
theorem WithTop.coe_sum {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (s : Finset ι) (f : ιM) :
(∑ is, f i) = is, (f i)
@[simp]
theorem WithTop.sum_eq_top {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {s : Finset ι} {f : ιWithTop M} :
is, f i = is, f i =

A sum is infinite iff one term is infinite.

theorem WithTop.sum_ne_top {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {s : Finset ι} {f : ιWithTop M} :
is, f i is, f i

A sum is finite iff all terms are finite.

@[simp]
theorem WithTop.sum_lt_top {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {s : Finset ι} {f : ιWithTop M} [LT M] :
is, f i < is, f i <

A sum is finite iff all terms are finite.

theorem WithTop.prod_ne_top {ι : Type u_1} {M₀ : Type u_3} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] [DecidableEq M₀] {s : Finset ι} {f : ιWithTop M₀} (h : is, f i ) :
is, f i

A product of finite terms is finite.

theorem WithTop.prod_lt_top {ι : Type u_1} {M₀ : Type u_3} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] [DecidableEq M₀] {s : Finset ι} {f : ιWithTop M₀} [LT M₀] (h : is, f i < ) :
is, f i <

A product of finite terms is finite.

@[simp]
theorem WithBot.coe_sum {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (s : Finset ι) (f : ιM) :
(∑ is, f i) = is, (f i)
theorem WithBot.sum_eq_bot_iff {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {s : Finset ι} {f : ιWithBot M} :
is, f i = is, f i =

A sum is infinite iff one term is infinite.

theorem WithBot.bot_lt_sum_iff {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {s : Finset ι} {f : ιWithBot M} [LT M] :
< is, f i is, < f i

A sum is finite iff all terms are finite.

theorem WithBot.sum_lt_bot {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {s : Finset ι} {f : ιWithBot M} [LT M] (h : is, f i ) :
< is, f i

A sum of finite terms is finite.

theorem WithBot.prod_ne_bot {ι : Type u_1} {M₀ : Type u_3} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] [DecidableEq M₀] {s : Finset ι} {f : ιWithBot M₀} (h : is, f i ) :
is, f i

A product of finite terms is finite.

theorem WithBot.bot_lt_prod {ι : Type u_1} {M₀ : Type u_3} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] [DecidableEq M₀] {s : Finset ι} {f : ιWithBot M₀} [LT M₀] (h : is, < f i) :
< is, f i

A product of finite terms is finite.