Documentation

Mathlib.Algebra.BigOperators.GroupWithZero.Finset

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) :
js, 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 ι} :
(∏ is, if p i then f i else 0) = if is, p i then is, f i else 0
theorem Finset.prod_boole {ι : Type u_1} {M₀ : Type u_4} [CommMonoidWithZero M₀] {p : ιProp} [DecidablePred p] {s : Finset ι} :
(∏ is, if p i then 1 else 0) = if is, 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 : κ) => is, f i x) is, 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₀] :
xs, f x = 0 as, 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₀] :
xs, f x 0 as, 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 : κ) => is, f i j) = is, 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 : is, f i 0) :
Units.mk0 (∏ is, f i) h = is.attach, Units.mk0 (f i)