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)

@[simp]

theorem Set.indicator_pi_one_apply {ι : Type u_1} {M₀ : Type u_4} {α : ι → Type u_5} [CommMonoidWithZero M₀] (s : Finset ι) (t : (i : ι) → Set (α i)) (f : (i : ι) → α i) : ((↑s).pi t).indicator 1 f = ∏ i ∈ s, (t i).indicator 1 (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) ⋯