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₀] :

∏ x ∈ s, f x = 0 ↔ ∃ a ∈ s, f a = 0

theorem Finset.prod_ne_zero_iff {ι : Type u_1} {M₀ : Type u_4} [CommMonoidWithZero M₀] {f : ι → M₀} {s : Finset ι} [Nontrivial M₀] [NoZeroDivisors M₀] :

∏ x ∈ s, f x ≠ 0 ↔ ∀ a ∈ s, f a ≠ 0

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) :

mk0 (∏ i ∈ s, f i) h = ∏ i ∈ s.attach, mk0 (f ↑i) ⋯

Documentation