Big operators on a finset in groups with zero #
This file contains the results concerning the interaction of finset big operators with groups with zero.
theorem
Finset.prod_eq_zero
{ι : Type u_1}
{M₀ : Type u_4}
[CommMonoidWithZero M₀]
{f : ι → M₀}
{s : Finset ι}
{i : ι}
(hi : i ∈ s)
(h : f i = 0)
:
∏ j ∈ s, f j = 0
theorem
Finset.prod_ite_zero
{ι : Type u_1}
{M₀ : Type u_4}
[CommMonoidWithZero M₀]
{p : ι → Prop}
[DecidablePred p]
{f : ι → M₀}
{s : Finset ι}
:
(∏ i ∈ s, if p i then f i else 0) = if ∀ i ∈ s, p i then ∏ i ∈ s, f i else 0
theorem
Finset.prod_boole
{ι : Type u_1}
{M₀ : Type u_4}
[CommMonoidWithZero M₀]
{p : ι → Prop}
[DecidablePred p]
{s : Finset ι}
:
(∏ i ∈ s, if p i then 1 else 0) = if ∀ i ∈ s, p i then 1 else 0
theorem
Finset.support_prod_subset
{ι : Type u_1}
{κ : Type u_2}
{M₀ : Type u_4}
[CommMonoidWithZero M₀]
(s : Finset ι)
(f : ι → κ → M₀)
:
(Function.support fun (x : κ) => ∏ i ∈ s, f i x) ⊆ ⋂ i ∈ s, Function.support (f i)
theorem
Finset.prod_eq_zero_iff
{ι : Type u_1}
{M₀ : Type u_4}
[CommMonoidWithZero M₀]
{f : ι → M₀}
{s : Finset ι}
[Nontrivial M₀]
[NoZeroDivisors M₀]
:
theorem
Finset.prod_ne_zero_iff
{ι : Type u_1}
{M₀ : Type u_4}
[CommMonoidWithZero M₀]
{f : ι → M₀}
{s : Finset ι}
[Nontrivial M₀]
[NoZeroDivisors M₀]
:
theorem
Finset.support_prod
{ι : Type u_1}
{κ : Type u_2}
{M₀ : Type u_4}
[CommMonoidWithZero M₀]
[Nontrivial M₀]
[NoZeroDivisors M₀]
(s : Finset ι)
(f : ι → κ → M₀)
:
(Function.support fun (j : κ) => ∏ i ∈ s, f i j) = ⋂ i ∈ s, Function.support (f i)
theorem
Fintype.prod_ite_zero
{ι : Type u_1}
{M₀ : Type u_4}
[Fintype ι]
[CommMonoidWithZero M₀]
{p : ι → Prop}
[DecidablePred p]
{f : ι → M₀}
:
(∏ i : ι, if p i then f i else 0) = if ∀ (i : ι), p i then ∏ i : ι, f i else 0
theorem
Fintype.prod_boole
{ι : Type u_1}
{M₀ : Type u_4}
[Fintype ι]
[CommMonoidWithZero M₀]
{p : ι → Prop}
[DecidablePred p]
:
(∏ i : ι, if p i then 1 else 0) = if ∀ (i : ι), p i then 1 else 0
theorem
Units.mk0_prod
{ι : Type u_1}
{G₀ : Type u_3}
[CommGroupWithZero G₀]
(s : Finset ι)
(f : ι → G₀)
(h : ∏ i ∈ s, f i ≠ 0)
: