Mathlib.Algebra.BigOperators.GroupWithZero.Finset

Finset.prod_eq_zero theorem

(hi : i ∈ s) (h : f i = 0) : ∏ j ∈ s, f j = 0

Full source

lemma prod_eq_zero (hi : i ∈ s) (h : f i = 0) : ∏ j ∈ s, f j = 0 := by
  classical rw [← prod_erase_mul _ _ hi, h, mul_zero]

Product over a finite set vanishes if any factor is zero

Informal description

Let $s$ be a finite set, $i$ an element of $s$, and $f : \alpha \to \beta$ a function where $\beta$ is a commutative monoid with zero. If $f(i) = 0$, then the product $\prod_{j \in s} f(j) = 0$.

Finset.prod_ite_zero theorem

: (∏ i ∈ s, if p i then f i else 0) = if ∀ i ∈ s, p i then ∏ i ∈ s, f i else 0

Full source

lemma prod_ite_zero :
    (∏ i ∈ s, if p i then f i else 0) = if ∀ i ∈ s, p i then ∏ i ∈ s, f i else 0 := by
  split_ifs with h
  · exact prod_congr rfl fun i hi => by simp [h i hi]
  · push_neg at h
    rcases h with ⟨i, hi, hq⟩
    exact prod_eq_zero hi (by simp [hq])

Product of Conditional Terms over Finite Set: $\prod_{i \in s} (p(i) ? f(i) : 0) = (\forall i \in s, p(i)) ? \prod_{i \in s} f(i) : 0$

Informal description

Let $s$ be a finite set, $p$ a predicate on elements of $s$, and $f$ a function from elements of $s$ to a commutative monoid with zero. Then the product $\prod_{i \in s} ( \text{if } p(i) \text{ then } f(i) \text{ else } 0 )$ equals $\prod_{i \in s} f(i)$ if $p(i)$ holds for all $i \in s$, and equals $0$ otherwise.

Finset.prod_boole theorem

: ∏ i ∈ s, (ite (p i) 1 0 : M₀) = ite (∀ i ∈ s, p i) 1 0

Full source

lemma prod_boole : ∏ i ∈ s, (ite (p i) 1 0 : M₀) = ite (∀ i ∈ s, p i) 1 0 := by
  rw [prod_ite_zero, prod_const_one]

Product of Indicator Functions over Finite Set: $\prod_{i \in s} (p(i) ? 1 : 0) = (\forall i \in s, p(i)) ? 1 : 0$

Informal description

Let $s$ be a finite set, $p$ a predicate on elements of $s$, and $M_0$ a commutative monoid with zero. Then the product $\prod_{i \in s} (\text{if } p(i) \text{ then } 1 \text{ else } 0)$ equals $1$ if $p(i)$ holds for all $i \in s$, and equals $0$ otherwise.

Finset.support_prod_subset theorem

(s : Finset ι) (f : ι → κ → M₀) : support (fun x ↦ ∏ i ∈ s, f i x) ⊆ ⋂ i ∈ s, support (f i)

Full source

lemma support_prod_subset (s : Finset ι) (f : ι → κ → M₀) :
    supportsupport (fun x ↦ ∏ i ∈ s, f i x) ⊆ ⋂ i ∈ s, support (f i) :=
  fun _ hx ↦ Set.mem_iInter₂.2 fun _ hi H ↦ hx <| prod_eq_zero hi H

Support of Product Function is Contained in Intersection of Supports

Informal description

Let $s$ be a finite set of indices, and for each $i \in s$, let $f_i : \kappa \to M_0$ be a function to a commutative monoid with zero. The support of the product function $x \mapsto \prod_{i \in s} f_i(x)$ is contained in the intersection of the supports of the individual functions $f_i$: $$\text{support}\left(\prod_{i \in s} f_i\right) \subseteq \bigcap_{i \in s} \text{support}(f_i).$$

Finset.prod_eq_zero_iff theorem

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

Full source

lemma prod_eq_zero_iff : ∏ x ∈ s, f x∏ x ∈ s, f x = 0 ↔ ∃ a ∈ s, f a = 0 := by
  classical
    induction s using Finset.induction_on with
    | empty => exact ⟨Not.elim one_ne_zero, fun ⟨_, H, _⟩ => by simp at H⟩
    | insert _ _ ha ih => rw [prod_insert ha, mul_eq_zero, exists_mem_insert, ih]

Product Equals Zero Iff Some Factor is Zero

Informal description

For a finite set $s$ and a function $f$ mapping elements of $s$ to a commutative monoid with zero, the product $\prod_{x \in s} f(x)$ equals zero if and only if there exists an element $a \in s$ such that $f(a) = 0$.

Finset.prod_ne_zero_iff theorem

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

Full source

lemma prod_ne_zero_iff : ∏ x ∈ s, f x∏ x ∈ s, f x ≠ 0∏ x ∈ s, f x ≠ 0 ↔ ∀ a ∈ s, f a ≠ 0 := by
  rw [Ne, prod_eq_zero_iff]
  push_neg; rfl

Nonzero Product Iff All Factors Nonzero in Finite Set

Informal description

For a finite set $s$ and a function $f$ mapping elements of $s$ to a commutative monoid with zero, the product $\prod_{x \in s} f(x)$ is nonzero if and only if $f(a) \neq 0$ for every $a \in s$.

Finset.support_prod theorem

(s : Finset ι) (f : ι → κ → M₀) : support (fun j ↦ ∏ i ∈ s, f i j) = ⋂ i ∈ s, support (f i)

Full source

lemma support_prod (s : Finset ι) (f : ι → κ → M₀) :
    support (fun j ↦ ∏ i ∈ s, f i j) = ⋂ i ∈ s, support (f i) :=
  Set.ext fun x ↦ by simp [support, prod_eq_zero_iff]

Support of Product Function Equals Intersection of Supports

Informal description

For a finite set $s$ of indices of type $\iota$ and a family of functions $f : \iota \to \kappa \to M₀$ (where $M₀$ is a type with zero), the support of the product function $\prod_{i \in s} f(i)$ is equal to the intersection of the supports of the individual functions $f(i)$ for $i \in s$. That is, \[ \text{support}\left(\lambda j, \prod_{i \in s} f(i)(j)\right) = \bigcap_{i \in s} \text{support}(f(i)). \] Here, the support of a function $g : \kappa \to M₀$ is the set $\{j \in \kappa \mid g(j) \neq 0\}$.

Fintype.prod_ite_zero theorem

: (∏ i, if p i then f i else 0) = if ∀ i, p i then ∏ i, f i else 0

Full source

lemma prod_ite_zero : (∏ i, if p i then f i else 0) = if ∀ i, p i then ∏ i, f i else 0 := by
  simp [Finset.prod_ite_zero]

Product of Conditional Terms over Finite Type: $\prod_i (p(i) ? f(i) : 0) = (\forall i, p(i)) ? \prod_i f(i) : 0$

Informal description

Let $\alpha$ be a finite type, $p$ a predicate on $\alpha$, and $f$ a function from $\alpha$ to a commutative monoid with zero. Then the product $\prod_{i \in \alpha} ( \text{if } p(i) \text{ then } f(i) \text{ else } 0 )$ equals $\prod_{i \in \alpha} f(i)$ if $p(i)$ holds for all $i \in \alpha$, and equals $0$ otherwise.

Fintype.prod_boole theorem

: ∏ i, (ite (p i) 1 0 : M₀) = ite (∀ i, p i) 1 0

Full source

lemma prod_boole : ∏ i, (ite (p i) 1 0 : M₀) = ite (∀ i, p i) 1 0 := by simp [Finset.prod_boole]

Product of Indicator Functions over Finite Type: $\prod_i (p(i) ? 1 : 0) = (\forall i, p(i)) ? 1 : 0$

Informal description

For a finite type $\alpha$, a predicate $p : \alpha \to \text{Prop}$, and a commutative monoid with zero $M_0$, the product $\prod_{i \in \alpha} (p(i) ? 1 : 0)$ equals $1$ if $p(i)$ holds for all $i \in \alpha$, and equals $0$ otherwise. Here, $p(i) ? 1 : 0$ denotes the indicator function that returns $1$ if $p(i)$ is true and $0$ otherwise.

Units.mk0_prod theorem

 [CommGroupWithZero G₀] (s : Finset ι) (f : ι → G₀) (h) :
  Units.mk0 (∏ i ∈ s, f i) h = ∏ i ∈ s.attach, Units.mk0 (f i) fun hh ↦ h (Finset.prod_eq_zero i.2 hh)

Full source

lemma Units.mk0_prod [CommGroupWithZero G₀] (s : Finset ι) (f : ι → G₀) (h) :
    Units.mk0 (∏ i ∈ s, f i) h =
      ∏ i ∈ s.attach, Units.mk0 (f i) fun hh ↦ h (Finset.prod_eq_zero i.2 hh) := by
  classical induction s using Finset.induction_on <;> simp [*]

Construction of Units from Nonzero Product Equals Product of Unit Constructions

Informal description

Let $G_0$ be a commutative group with zero, $s$ a finite set of indices, and $f : \iota \to G_0$ a function. For any proof $h$ that the product $\prod_{i \in s} f(i)$ is nonzero, the unit element constructed from this product equals the product over the attached set of $s$ of the unit elements constructed from each $f(i)$, where the proof that each $f(i)$ is nonzero is derived from $h$ and the fact that if any $f(i) = 0$, the product would be zero. In symbols: \[ \text{Units.mk0}\left(\prod_{i \in s} f(i), h\right) = \prod_{i \in s.\text{attach}} \text{Units.mk0}(f(i), \lambda hh \mapsto h (\text{Finset.prod\_eq\_zero}\ i.2\ hh)) \]