Mathlib.Algebra.BigOperators.Finprod

finsum definition

Full source

/-- Sum of `f x` as `x` ranges over the elements of the support of `f`, if it's finite. Zero
otherwise. -/
noncomputable irreducible_def finsum (lemma := finsum_def') [AddCommMonoid M] (f : α → M) : M :=
  if h : (support (f ∘ PLift.down)).Finite then ∑ i ∈ h.toFinset, f i.down else 0

Finite sum over a possibly infinite type

Informal description

Given an additive commutative monoid $M$ and a function $f : \alpha \to M$, the sum $\sumᶠ x, f x$ is defined as the sum of $f x$ over all $x$ in the support of $f$ if this support is finite, and zero otherwise. Here, the support of $f$ is the set of elements $x \in \alpha$ for which $f x \neq 0$.

finsum_def' theorem

: eta_helper Eq✝ @finsum.{} @(delta% @definition✝)

Full source

/-- Sum of `f x` as `x` ranges over the elements of the support of `f`, if it's finite. Zero
otherwise. -/
noncomputable irreducible_def finsum (lemma := finsum_def') [AddCommMonoid M] (f : α → M) : M :=
  if h : (support (f ∘ PLift.down)).Finite then ∑ i ∈ h.toFinset, f i.down else 0

Definition of finite sum via support

Informal description

Let $M$ be an additive commutative monoid and $f : \alpha \to M$ be a function. The finite sum $\sumᶠ x, f x$ is equal to the sum of $f x$ over the finite set $\{x \mid f x \neq 0\}$ if this set is finite, and zero otherwise.

finprod definition

Full source

/-- Product of `f x` as `x` ranges over the elements of the multiplicative support of `f`, if it's
finite. One otherwise. -/
@[to_additive existing]
noncomputable irreducible_def finprod (lemma := finprod_def') (f : α → M) : M :=
  if h : (mulSupport (f ∘ PLift.down)).Finite then ∏ i ∈ h.toFinset, f i.down else 1

Finite product over a type

Informal description

The function `finprod` takes a function $f : \alpha \to M$ where $M$ is a commutative monoid, and returns the product of $f(x)$ over all $x$ in the multiplicative support of $f$ (i.e., the set of $x$ where $f(x) \neq 1$). If this support is finite, the result is the finite product $\prod_{x \in \text{supp}(f)} f(x)$. If the support is infinite, the result is defined to be $1$.

finprod_def' theorem

: eta_helper Eq✝ @finprod.{} @(delta% @definition✝)

Full source

/-- Product of `f x` as `x` ranges over the elements of the multiplicative support of `f`, if it's
finite. One otherwise. -/
@[to_additive existing]
noncomputable irreducible_def finprod (lemma := finprod_def') (f : α → M) : M :=
  if h : (mulSupport (f ∘ PLift.down)).Finite then ∏ i ∈ h.toFinset, f i.down else 1

Definition of Finite Product via Multiplicative Support

Informal description

The finite product function `finprod` is defined as follows: for a function $f : \alpha \to M$ where $M$ is a commutative monoid, if the multiplicative support of $f$ (the set $\{x \in \alpha \mid f(x) \neq 1\}$) is finite, then $\prodᶠ f = \prod_{x \in \text{supp}(f)} f(x)$; otherwise, $\prodᶠ f = 1$.

term∑ᶠ_,_ definition

: Lean.ParserDescr✝

Full source

/-- `∑ᶠ x, f x` is notation for `finsum f`. It is the sum of `f x`, where `x` ranges over the
support of `f`, if it's finite, zero otherwise. Taking the sum over multiple arguments or
conditions is possible, e.g. `∏ᶠ (x) (y), f x y` and `∏ᶠ (x) (h: x ∈ s), f x` -/
notation3"∑ᶠ "(...)", "r:67:(scoped f => finsum f) => r

Finite sum notation

Informal description

The notation $\sumᶠ x, f x$ represents the sum of $f x$ over all $x$ in the support of $f$, if this support is finite. If the support is infinite, the sum is defined to be zero. This notation can also be used with multiple arguments or conditions, such as $\sumᶠ (x) (y), f x y$ or $\sumᶠ (x) (h : x \in s), f x$.

term∑ᶠ_,_.delab_app.finsum definition

: Delab✝

Full source

/-- `∑ᶠ x, f x` is notation for `finsum f`. It is the sum of `f x`, where `x` ranges over the
support of `f`, if it's finite, zero otherwise. Taking the sum over multiple arguments or
conditions is possible, e.g. `∏ᶠ (x) (y), f x y` and `∏ᶠ (x) (h: x ∈ s), f x` -/
notation3"∑ᶠ "(...)", "r:67:(scoped f => finsum f) => r

Finite sum notation

Informal description

The notation $\sumᶠ x, f x$ represents the sum of $f x$ over all $x$ in the support of $f$, where the support is finite. If the support is infinite, the sum is defined to be zero. This notation can be extended to multiple arguments or conditions, such as $\sumᶠ (x) (y), f x y$ or $\sumᶠ (x) (h : x \in s), f x$.

term∏ᶠ_,_ definition

: Lean.ParserDescr✝

Full source

/-- `∏ᶠ x, f x` is notation for `finprod f`. It is the product of `f x`, where `x` ranges over the
multiplicative support of `f`, if it's finite, one otherwise. Taking the product over multiple
arguments or conditions is possible, e.g. `∏ᶠ (x) (y), f x y` and `∏ᶠ (x) (h: x ∈ s), f x` -/
notation3"∏ᶠ "(...)", "r:67:(scoped f => finprod f) => r

Finite product notation

Informal description

The notation `∏ᶠ x, f x` represents the product of `f x` over all `x` in the multiplicative support of `f`, if this support is finite. If the support is infinite, the product is defined to be 1. This notation can also be used with multiple arguments or conditions, such as `∏ᶠ (x) (y), f x y` or `∏ᶠ (x) (h : x ∈ s), f x`.

term∏ᶠ_,_.delab_app.finprod definition

: Delab✝

Full source

/-- `∏ᶠ x, f x` is notation for `finprod f`. It is the product of `f x`, where `x` ranges over the
multiplicative support of `f`, if it's finite, one otherwise. Taking the product over multiple
arguments or conditions is possible, e.g. `∏ᶠ (x) (y), f x y` and `∏ᶠ (x) (h: x ∈ s), f x` -/
notation3"∏ᶠ "(...)", "r:67:(scoped f => finprod f) => r

Finite product notation

Informal description

The notation `∏ᶠ x, f x` represents the finite product of `f x` over all `x` in the multiplicative support of `f`. If the support is finite, it computes the product; otherwise, it defaults to 1. This notation can be extended to multiple arguments or conditions, such as `∏ᶠ (x) (y), f x y` or `∏ᶠ (x) (h : x ∈ s), f x`.

finprod_eq_prod_plift_of_mulSupport_toFinset_subset theorem

 {f : α → M} (hf : (mulSupport (f ∘ PLift.down)).Finite) {s : Finset (PLift α)} (hs : hf.toFinset ⊆ s) :
  ∏ᶠ i, f i = ∏ i ∈ s, f i.down

Full source

@[to_additive]
theorem finprod_eq_prod_plift_of_mulSupport_toFinset_subset {f : α → M}
    (hf : (mulSupport (f ∘ PLift.down)).Finite) {s : Finset (PLift α)} (hs : hf.toFinset ⊆ s) :
    ∏ᶠ i, f i = ∏ i ∈ s, f i.down := by
  rw [finprod, dif_pos]
  refine Finset.prod_subset hs fun x _ hxf => ?_
  rwa [hf.mem_toFinset, nmem_mulSupport] at hxf

Finite Product Equals Finset Product When Support is Contained in Finset

Informal description

Let $f : \alpha \to M$ be a function where $M$ is a commutative monoid, and suppose the multiplicative support of $f \circ \mathrm{PLift.down}$ is finite. For any finite subset $s$ of $\mathrm{PLift} \alpha$ containing the finset representation of this support, the finite product $\prodᶠ_{i} f(i)$ equals the product $\prod_{i \in s} f(i.\mathrm{down})$.

finprod_eq_prod_plift_of_mulSupport_subset theorem

 {f : α → M} {s : Finset (PLift α)} (hs : mulSupport (f ∘ PLift.down) ⊆ s) : ∏ᶠ i, f i = ∏ i ∈ s, f i.down

Full source

@[to_additive]
theorem finprod_eq_prod_plift_of_mulSupport_subset {f : α → M} {s : Finset (PLift α)}
    (hs : mulSupportmulSupport (f ∘ PLift.down) ⊆ s) : ∏ᶠ i, f i = ∏ i ∈ s, f i.down :=
  finprod_eq_prod_plift_of_mulSupport_toFinset_subset (s.finite_toSet.subset hs) fun x hx => by
    rw [Finite.mem_toFinset] at hx
    exact hs hx

Finite Product Equals Finset Product When Support is Subset

Informal description

Let $f : \alpha \to M$ be a function where $M$ is a commutative monoid, and let $s$ be a finite subset of $\mathrm{PLift} \alpha$. If the multiplicative support of $f \circ \mathrm{PLift.down}$ is contained in $s$, then the finite product $\prodᶠ_{i} f(i)$ equals the product $\prod_{i \in s} f(i.\mathrm{down})$.

finprod_one theorem

: (∏ᶠ _ : α, (1 : M)) = 1

Full source

@[to_additive (attr := simp)]
theorem finprod_one : (∏ᶠ _ : α, (1 : M)) = 1 := by
  have : (mulSupport fun x : PLift α => (fun _ => 1 : α → M) x.down) ⊆ (∅ : Finset (PLift α)) :=
    fun x h => by simp at h
  rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_empty]

Finite Product of Constant One Function is One

Informal description

The finite product of the constant function $f(x) = 1$ over any type $\alpha$ is equal to $1$, i.e., $\prodᶠ_{x \in \alpha} 1 = 1$.

finprod_of_isEmpty theorem

[IsEmpty α] (f : α → M) : ∏ᶠ i, f i = 1

Full source

@[to_additive]
theorem finprod_of_isEmpty [IsEmpty α] (f : α → M) : ∏ᶠ i, f i = 1 := by
  rw [← finprod_one]
  congr
  simp [eq_iff_true_of_subsingleton]

Finite product over empty type is one

Informal description

For any empty type $\alpha$ and any function $f : \alpha \to M$ where $M$ is a commutative monoid, the finite product $\prodᶠ_{i \in \alpha} f(i)$ equals $1$.

finprod_false theorem

(f : False → M) : ∏ᶠ i, f i = 1

Full source

@[to_additive (attr := simp)]
theorem finprod_false (f : False → M) : ∏ᶠ i, f i = 1 :=
  finprod_of_isEmpty _

Finite product over false is one

Informal description

For any function $f : \text{False} \to M$ where $M$ is a commutative monoid, the finite product $\prodᶠ_{i \in \text{False}} f(i)$ equals $1$.

finprod_eq_single theorem

(f : α → M) (a : α) (ha : ∀ x, x ≠ a → f x = 1) : ∏ᶠ x, f x = f a

Full source

@[to_additive]
theorem finprod_eq_single (f : α → M) (a : α) (ha : ∀ x, x ≠ a → f x = 1) :
    ∏ᶠ x, f x = f a := by
  have : mulSupportmulSupport (f ∘ PLift.down) ⊆ ({PLift.up a} : Finset (PLift α)) := by
    intro x
    contrapose
    simpa [PLift.eq_up_iff_down_eq] using ha x.down
  rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_singleton]

Finite product of a function with singleton support equals its value at that point

Informal description

Let $f : \alpha \to M$ be a function where $M$ is a commutative monoid, and let $a \in \alpha$ be such that $f(x) = 1$ for all $x \neq a$. Then the finite product $\prodᶠ_{x} f(x)$ equals $f(a)$.

finprod_unique theorem

[Unique α] (f : α → M) : ∏ᶠ i, f i = f default

Full source

@[to_additive]
theorem finprod_unique [Unique α] (f : α → M) : ∏ᶠ i, f i = f default :=
  finprod_eq_single f default fun _x hx => (hx <| Unique.eq_default _).elim

Finite product over a unique type equals evaluation at the default element

Informal description

Let $\alpha$ be a type with a unique element (denoted as `default`), and let $M$ be a commutative monoid. For any function $f : \alpha \to M$, the finite product $\prodᶠ_{i} f(i)$ equals $f(\text{default})$.

finprod_true theorem

(f : True → M) : ∏ᶠ i, f i = f trivial

Full source

@[to_additive (attr := simp)]
theorem finprod_true (f : True → M) : ∏ᶠ i, f i = f trivial :=
  @finprod_unique M True _ ⟨⟨trivial⟩, fun _ => rfl⟩ f

Finite product over the true type equals evaluation at trivial

Informal description

For any commutative monoid $M$ and any function $f : \text{True} \to M$, the finite product $\prodᶠ_{i} f(i)$ equals $f(\text{trivial})$, where $\text{trivial}$ is the unique element of the type $\text{True}$.

finprod_eq_dif theorem

{p : Prop} [Decidable p] (f : p → M) : ∏ᶠ i, f i = if h : p then f h else 1

Full source

@[to_additive]
theorem finprod_eq_dif {p : Prop} [Decidable p] (f : p → M) :
    ∏ᶠ i, f i = if h : p then f h else 1 := by
  split_ifs with h
  · haveI : Unique p := ⟨⟨h⟩, fun _ => rfl⟩
    exact finprod_unique f
  · haveI : IsEmpty p := ⟨h⟩
    exact finprod_of_isEmpty f

Finite product over a decidable proposition equals conditional evaluation

Informal description

Let $p$ be a proposition with a decidable instance, and let $f : p \to M$ be a function from $p$ to a commutative monoid $M$. The finite product $\prodᶠ_{i \in p} f(i)$ equals $f(h)$ if $p$ holds (with witness $h : p$), and equals $1$ otherwise.

finprod_eq_if theorem

{p : Prop} [Decidable p] {x : M} : ∏ᶠ _ : p, x = if p then x else 1

Full source

@[to_additive]
theorem finprod_eq_if {p : Prop} [Decidable p] {x : M} : ∏ᶠ _ : p, x = if p then x else 1 :=
  finprod_eq_dif fun _ => x

Finite product over a proposition: $\prodᶠ_{i \in p} x = \text{if } p \text{ then } x \text{ else } 1$

Informal description

For any proposition $p$ with a decidable instance and any element $x$ in a commutative monoid $M$, the finite product $\prodᶠ_{i \in p} x$ equals $x$ if $p$ holds, and equals $1$ otherwise.

finprod_congr theorem

{f g : α → M} (h : ∀ x, f x = g x) : finprod f = finprod g

Full source

@[to_additive]
theorem finprod_congr {f g : α → M} (h : ∀ x, f x = g x) : finprod f = finprod g :=
  congr_arg _ <| funext h

Equality of Finite Products under Pointwise Equality of Functions

Informal description

For any two functions $f, g : \alpha \to M$ from a type $\alpha$ to a commutative monoid $M$, if $f(x) = g(x)$ for all $x \in \alpha$, then the finite products $\prodᶠ_{x} f(x)$ and $\prodᶠ_{x} g(x)$ are equal.

finprod_congr_Prop theorem

{p q : Prop} {f : p → M} {g : q → M} (hpq : p = q) (hfg : ∀ h : q, f (hpq.mpr h) = g h) : finprod f = finprod g

Full source

@[to_additive (attr := congr)]
theorem finprod_congr_Prop {p q : Prop} {f : p → M} {g : q → M} (hpq : p = q)
    (hfg : ∀ h : q, f (hpq.mpr h) = g h) : finprod f = finprod g := by
  subst q
  exact finprod_congr hfg

Equality of Finite Products under Propositional Equality

Informal description

Let $p$ and $q$ be propositions such that $p = q$, and let $f : p \to M$ and $g : q \to M$ be functions into a commutative monoid $M$. If for every $h : q$ we have $f(hpq^{-1}(h)) = g(h)$, where $hpq^{-1}$ is the proof of $q \to p$ obtained from $hpq$, then the finite products $\prodᶠ_{i} f(i)$ and $\prodᶠ_{i} g(i)$ are equal.

finprod_induction theorem

 {f : α → M} (p : M → Prop) (hp₀ : p 1) (hp₁ : ∀ x y, p x → p y → p (x * y)) (hp₂ : ∀ i, p (f i)) : p (∏ᶠ i, f i)

Full source

/-- To prove a property of a finite product, it suffices to prove that the property is
multiplicative and holds on the factors. -/
@[to_additive
      "To prove a property of a finite sum, it suffices to prove that the property is
      additive and holds on the summands."]
theorem finprod_induction {f : α → M} (p : M → Prop) (hp₀ : p 1)
    (hp₁ : ∀ x y, p x → p y → p (x * y)) (hp₂ : ∀ i, p (f i)) : p (∏ᶠ i, f i) := by
  rw [finprod]
  split_ifs
  exacts [Finset.prod_induction _ _ hp₁ hp₀ fun i _ => hp₂ _, hp₀]

Induction Principle for Finite Products in Commutative Monoids

Informal description

Let $M$ be a commutative monoid and $f : \alpha \to M$ a function. For any predicate $p : M \to \mathrm{Prop}$ satisfying: 1. $p(1)$ holds, 2. $p$ is multiplicative (i.e., $p(x)$ and $p(y)$ imply $p(x \cdot y)$ for all $x, y \in M$), 3. $p(f(i))$ holds for all $i \in \alpha$, then $p\left(\prodᶠ_{i} f(i)\right)$ holds, where $\prodᶠ$ denotes the finite product over the multiplicative support of $f$.

finprod_nonneg theorem

 {R : Type*} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] {f : α → R} (hf : ∀ x, 0 ≤ f x) : 0 ≤ ∏ᶠ x, f x

Full source

theorem finprod_nonneg {R : Type*} [CommSemiring R] [PartialOrder R] [IsOrderedRing R]
    {f : α → R} (hf : ∀ x, 0 ≤ f x) :
    0 ≤ ∏ᶠ x, f x :=
  finprod_induction (fun x => 0 ≤ x) zero_le_one (fun _ _ => mul_nonneg) hf

Nonnegativity of Finite Products in Ordered Semirings

Informal description

Let $R$ be a commutative semiring equipped with a partial order $\leq$ and the structure of an ordered ring. For any function $f : \alpha \to R$ such that $f(x) \geq 0$ for all $x \in \alpha$, the finite product $\prodᶠ_{x} f(x)$ is nonnegative, i.e., $0 \leq \prodᶠ_{x} f(x)$.

one_le_finprod' theorem

 {M : Type*} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] {f : α → M} (hf : ∀ i, 1 ≤ f i) : 1 ≤ ∏ᶠ i, f i

Full source

@[to_additive finsum_nonneg]
theorem one_le_finprod' {M : Type*} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M]
    {f : α → M} (hf : ∀ i, 1 ≤ f i) :
    1 ≤ ∏ᶠ i, f i :=
  finprod_induction _ le_rfl (fun _ _ => one_le_mul) hf

Lower bound for finite products in ordered monoids: $1 \leq \prodᶠ_{i} f(i)$ when $1 \leq f(i)$ for all $i$

Informal description

Let $M$ be a commutative monoid equipped with a partial order such that it forms an ordered monoid. For any function $f : \alpha \to M$ satisfying $1 \leq f(i)$ for all $i \in \alpha$, the finite product $\prodᶠ_{i} f(i)$ satisfies $1 \leq \prodᶠ_{i} f(i)$.

MonoidHom.map_finprod_plift theorem

(f : M →* N) (g : α → M) (h : (mulSupport <| g ∘ PLift.down).Finite) : f (∏ᶠ x, g x) = ∏ᶠ x, f (g x)

Full source

@[to_additive]
theorem MonoidHom.map_finprod_plift (f : M →* N) (g : α → M)
    (h : (mulSupport <| g ∘ PLift.down).Finite) : f (∏ᶠ x, g x) = ∏ᶠ x, f (g x) := by
  rw [finprod_eq_prod_plift_of_mulSupport_subset h.coe_toFinset.ge,
    finprod_eq_prod_plift_of_mulSupport_subset, map_prod]
  rw [h.coe_toFinset]
  exact mulSupport_comp_subset f.map_one (g ∘ PLift.down)

Monoid homomorphism preserves finite product over lifted type

Informal description

Let $M$ and $N$ be commutative monoids, and let $f : M \to N$ be a monoid homomorphism. For any function $g : \alpha \to M$ such that the multiplicative support of $g \circ \mathrm{PLift.down}$ is finite, we have \[ f\left(\prodᶠ_{x} g(x)\right) = \prodᶠ_{x} f(g(x)). \]

MonoidHom.map_finprod_Prop theorem

{p : Prop} (f : M →* N) (g : p → M) : f (∏ᶠ x, g x) = ∏ᶠ x, f (g x)

Full source

@[to_additive]
theorem MonoidHom.map_finprod_Prop {p : Prop} (f : M →* N) (g : p → M) :
    f (∏ᶠ x, g x) = ∏ᶠ x, f (g x) :=
  f.map_finprod_plift g (Set.toFinite _)

Monoid homomorphism preserves finite product over propositions

Informal description

Let $M$ and $N$ be commutative monoids, and let $f \colon M \to N$ be a monoid homomorphism. For any proposition $p$ and any function $g \colon p \to M$, we have \[ f\left(\prodᶠ_{x} g(x)\right) = \prodᶠ_{x} f(g(x)). \]

MonoidHom.map_finprod_of_preimage_one theorem

(f : M →* N) (hf : ∀ x, f x = 1 → x = 1) (g : α → M) : f (∏ᶠ i, g i) = ∏ᶠ i, f (g i)

Full source

@[to_additive]
theorem MonoidHom.map_finprod_of_preimage_one (f : M →* N) (hf : ∀ x, f x = 1 → x = 1) (g : α → M) :
    f (∏ᶠ i, g i) = ∏ᶠ i, f (g i) := by
  by_cases hg : (mulSupport <| g ∘ PLift.down).Finite; · exact f.map_finprod_plift g hg
  rw [finprod, dif_neg, f.map_one, finprod, dif_neg]
  exacts [Infinite.mono (fun x hx => mt (hf (g x.down)) hx) hg, hg]

Monoid homomorphism preserves finite product when preimage of identity is identity

Informal description

Let $M$ and $N$ be commutative monoids, and let $f : M \to N$ be a monoid homomorphism. Suppose that for every $x \in M$, if $f(x) = 1$ then $x = 1$. Then for any function $g : \alpha \to M$, we have \[ f\left(\prodᶠ_{i} g(i)\right) = \prodᶠ_{i} f(g(i)). \]

MonoidHom.map_finprod_of_injective theorem

(g : M →* N) (hg : Injective g) (f : α → M) : g (∏ᶠ i, f i) = ∏ᶠ i, g (f i)

Full source

@[to_additive]
theorem MonoidHom.map_finprod_of_injective (g : M →* N) (hg : Injective g) (f : α → M) :
    g (∏ᶠ i, f i) = ∏ᶠ i, g (f i) :=
  g.map_finprod_of_preimage_one (fun _ => (hg.eq_iff' g.map_one).mp) f

Injective Monoid Homomorphism Preserves Finite Product

Informal description

Let $M$ and $N$ be commutative monoids, and let $g \colon M \to N$ be an injective monoid homomorphism. Then for any function $f \colon \alpha \to M$, we have \[ g\left(\prodᶠ_{i} f(i)\right) = \prodᶠ_{i} g(f(i)). \]

MulEquiv.map_finprod theorem

(g : M ≃* N) (f : α → M) : g (∏ᶠ i, f i) = ∏ᶠ i, g (f i)

Full source

@[to_additive]
theorem MulEquiv.map_finprod (g : M ≃* N) (f : α → M) : g (∏ᶠ i, f i) = ∏ᶠ i, g (f i) :=
  g.toMonoidHom.map_finprod_of_injective (EquivLike.injective g) f

Multiplicative Isomorphism Preserves Finite Product

Informal description

Let $M$ and $N$ be commutative monoids, and let $g \colon M \simeq^* N$ be a multiplicative equivalence (isomorphism) between them. Then for any function $f \colon \alpha \to M$, we have \[ g\left(\prodᶠ_{i} f(i)\right) = \prodᶠ_{i} g(f(i)). \]

MulEquivClass.map_finprod theorem

{F : Type*} [EquivLike F M N] [MulEquivClass F M N] (g : F) (f : α → M) : g (∏ᶠ i, f i) = ∏ᶠ i, g (f i)

Full source

@[to_additive]
theorem MulEquivClass.map_finprod {F : Type*} [EquivLike F M N] [MulEquivClass F M N] (g : F)
    (f : α → M) : g (∏ᶠ i, f i) = ∏ᶠ i, g (f i) :=
  MulEquiv.map_finprod (MulEquivClass.toMulEquiv g) f

Multiplicative Equivalence Preserves Finite Product

Informal description

Let $M$ and $N$ be commutative monoids, and let $F$ be a type equipped with an equivalence-like structure between $M$ and $N$ that preserves multiplication (i.e., $F$ is a `MulEquivClass`). For any multiplicative equivalence $g \in F$ and any function $f \colon \alpha \to M$, we have \[ g\left(\prodᶠ_{i} f(i)\right) = \prodᶠ_{i} g(f(i)). \]

finsum_smul theorem

 {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : ι → R) (x : M) :
  (∑ᶠ i, f i) • x = ∑ᶠ i, f i • x

Full source

/-- The `NoZeroSMulDivisors` makes sure that the result holds even when the support of `f` is
infinite. For a more usual version assuming `(support f).Finite` instead, see `finsum_smul'`. -/
theorem finsum_smul {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
    (f : ι → R) (x : M) : (∑ᶠ i, f i) • x = ∑ᶠ i, f i • x := by
  rcases eq_or_ne x 0 with (rfl | hx)
  · simp
  · exact ((smulAddHom R M).flip x).map_finsum_of_injective (smul_left_injective R hx) _

Distributivity of scalar multiplication over finite sum in modules without zero divisors

Informal description

Let $R$ be a ring and $M$ an additive commutative group with a module structure over $R$, such that $R$ and $M$ have no zero scalar divisors. For any function $f : \iota \to R$ and any element $x \in M$, the scalar multiplication of the sum $\sumᶠ_{i} f(i)$ with $x$ is equal to the sum $\sumᶠ_{i} (f(i) \cdot x)$.

smul_finsum theorem

 {R M : Type*} [Semiring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (c : R) (f : ι → M) :
  (c • ∑ᶠ i, f i) = ∑ᶠ i, c • f i

Full source

/-- The `NoZeroSMulDivisors` makes sure that the result holds even when the support of `f` is
infinite. For a more usual version assuming `(support f).Finite` instead, see `smul_finsum'`. -/
theorem smul_finsum {R M : Type*} [Semiring R] [AddCommGroup M] [Module R M]
    [NoZeroSMulDivisors R M] (c : R) (f : ι → M) : (c • ∑ᶠ i, f i) = ∑ᶠ i, c • f i := by
  rcases eq_or_ne c 0 with (rfl | hc)
  · simp
  · exact (smulAddHom R M c).map_finsum_of_injective (smul_right_injective M hc) _

Scalar Multiplication Distributes over Finite Sums in Modules without Zero Divisors

Informal description

Let $R$ be a semiring, $M$ an additive commutative group with an $R$-module structure, and assume $R$ and $M$ have no zero scalar divisors. For any scalar $c \in R$ and any function $f : \iota \to M$, the scalar multiplication of $c$ with the finite sum $\sumᶠ i, f i$ equals the finite sum of the scalar multiples $\sumᶠ i, c • f i$.

finprod_inv_distrib theorem

[DivisionCommMonoid G] (f : α → G) : (∏ᶠ x, (f x)⁻¹) = (∏ᶠ x, f x)⁻¹

Full source

@[to_additive]
theorem finprod_inv_distrib [DivisionCommMonoid G] (f : α → G) : (∏ᶠ x, (f x)⁻¹) = (∏ᶠ x, f x)⁻¹ :=
  ((MulEquiv.inv G).map_finprod f).symm

Inverse of Finite Product Equals Finite Product of Inverses in Commutative Division Monoid

Informal description

Let $G$ be a commutative division monoid and $f \colon \alpha \to G$ be a function. Then the finite product of the inverses of $f(x)$ equals the inverse of the finite product of $f(x)$, i.e., \[ \prodᶠ_{x} (f(x))^{-1} = \left(\prodᶠ_{x} f(x)\right)^{-1}. \]

finprod_eq_mulIndicator_apply theorem

(s : Set α) (f : α → M) (a : α) : ∏ᶠ _ : a ∈ s, f a = mulIndicator s f a

Full source

@[to_additive]
theorem finprod_eq_mulIndicator_apply (s : Set α) (f : α → M) (a : α) :
    ∏ᶠ _ : a ∈ s, f a = mulIndicator s f a := by
  classical convert finprod_eq_if (M := M) (p := a ∈ s) (x := f a)

Finite Product Equals Multiplicative Indicator Function

Informal description

For any set $s \subseteq \alpha$, function $f : \alpha \to M$ (where $M$ is a commutative monoid), and element $a \in \alpha$, the finite product $\prodᶠ_{a \in s} f(a)$ equals the multiplicative indicator function $\text{mulIndicator}\, s\, f\, a$, which is defined as: \[ \text{mulIndicator}\, s\, f\, a = \begin{cases} f(a) & \text{if } a \in s, \\ 1 & \text{otherwise.} \end{cases} \]

finprod_apply_ne_one theorem

(f : α → M) (a : α) : ∏ᶠ _ : f a ≠ 1, f a = f a

Full source

@[to_additive (attr := simp)]
theorem finprod_apply_ne_one (f : α → M) (a : α) : ∏ᶠ _ : f a ≠ 1, f a = f a := by
  rw [← mem_mulSupport, finprod_eq_mulIndicator_apply, mulIndicator_mulSupport]

Finite product over non-identity condition equals function value: $\prodᶠ_{f(a) \neq 1} f(a) = f(a)$

Informal description

For any function $f \colon \alpha \to M$ (where $M$ is a commutative monoid) and any element $a \in \alpha$, the finite product $\prodᶠ_{f(a) \neq 1} f(a)$ equals $f(a)$. In other words, when taking the finite product over the condition that $f(a) \neq 1$, the result is simply $f(a)$ itself.

finprod_mem_def theorem

(s : Set α) (f : α → M) : ∏ᶠ a ∈ s, f a = ∏ᶠ a, mulIndicator s f a

Full source

@[to_additive]
theorem finprod_mem_def (s : Set α) (f : α → M) : ∏ᶠ a ∈ s, f a = ∏ᶠ a, mulIndicator s f a :=
  finprod_congr <| finprod_eq_mulIndicator_apply s f

Finite Product over Set Equals Finite Product of Indicator Function

Informal description

For any set $s \subseteq \alpha$ and any function $f : \alpha \to M$ where $M$ is a commutative monoid, the finite product $\prodᶠ_{a \in s} f(a)$ equals the finite product $\prodᶠ_{a} \text{mulIndicator}_s f(a)$, where $\text{mulIndicator}_s f$ is the multiplicative indicator function defined as: \[ \text{mulIndicator}_s f(a) = \begin{cases} f(a) & \text{if } a \in s, \\ 1 & \text{otherwise.} \end{cases} \]

finprod_mem_mulSupport theorem

(f : α → M) : ∏ᶠ a ∈ mulSupport f, f a = ∏ᶠ a, f a

Full source

@[to_additive]
lemma finprod_mem_mulSupport (f : α → M) : ∏ᶠ a ∈ mulSupport f, f a = ∏ᶠ a, f a := by
  rw [finprod_mem_def, mulIndicator_mulSupport]

Finite Product over Multiplicative Support Equals Global Finite Product

Informal description

For any function $f \colon \alpha \to M$ where $M$ is a commutative monoid, the finite product $\prodᶠ_{a \in \text{mulSupport}(f)} f(a)$ over the multiplicative support of $f$ (i.e., the set $\{x \in \alpha \mid f(x) \neq 1\}$) equals the finite product $\prodᶠ_{a} f(a)$ over all elements of $\alpha$.

finprod_eq_prod_of_mulSupport_subset theorem

(f : α → M) {s : Finset α} (h : mulSupport f ⊆ s) : ∏ᶠ i, f i = ∏ i ∈ s, f i

Full source

@[to_additive]
theorem finprod_eq_prod_of_mulSupport_subset (f : α → M) {s : Finset α} (h : mulSupportmulSupport f ⊆ s) :
    ∏ᶠ i, f i = ∏ i ∈ s, f i := by
  have A : mulSupport (f ∘ PLift.down) = Equiv.pliftEquiv.plift.symm '' mulSupport f := by
    rw [mulSupport_comp_eq_preimage]
    exact (Equiv.plift.symm.image_eq_preimage _).symm
  have : mulSupportmulSupport (f ∘ PLift.down) ⊆ s.map Equiv.plift.symm.toEmbedding := by
    rw [A, Finset.coe_map]
    exact image_subset _ h
  rw [finprod_eq_prod_plift_of_mulSupport_subset this]
  simp only [Finset.prod_map, Equiv.coe_toEmbedding]
  congr

Finite Product Equals Finset Product When Support is Subset

Informal description

Let $f : \alpha \to M$ be a function where $M$ is a commutative monoid, and let $s$ be a finite subset of $\alpha$. If the multiplicative support of $f$ (i.e., the set $\{x \in \alpha \mid f(x) \neq 1\}$) is contained in $s$, then the finite product $\prodᶠ_{i} f(i)$ equals the finite product $\prod_{i \in s} f(i)$.

finprod_eq_prod_of_mulSupport_toFinset_subset theorem

(f : α → M) (hf : (mulSupport f).Finite) {s : Finset α} (h : hf.toFinset ⊆ s) : ∏ᶠ i, f i = ∏ i ∈ s, f i

Full source

@[to_additive]
theorem finprod_eq_prod_of_mulSupport_toFinset_subset (f : α → M) (hf : (mulSupport f).Finite)
    {s : Finset α} (h : hf.toFinset ⊆ s) : ∏ᶠ i, f i = ∏ i ∈ s, f i :=
  finprod_eq_prod_of_mulSupport_subset _ fun _ hx => h <| hf.mem_toFinset.2 hx

Finite Product Equals Finset Product When Support's Finset is Subset

Informal description

Let $f : \alpha \to M$ be a function where $M$ is a commutative monoid, and suppose the multiplicative support of $f$ (i.e., the set $\{x \in \alpha \mid f(x) \neq 1\}$) is finite with proof $hf$. For any finite subset $s$ of $\alpha$ such that the finset representation of the support is contained in $s$, the finite product $\prodᶠ_{i} f(i)$ equals the finite product $\prod_{i \in s} f(i)$.

finprod_eq_finset_prod_of_mulSupport_subset theorem

(f : α → M) {s : Finset α} (h : mulSupport f ⊆ (s : Set α)) : ∏ᶠ i, f i = ∏ i ∈ s, f i

Full source

@[to_additive]
theorem finprod_eq_finset_prod_of_mulSupport_subset (f : α → M) {s : Finset α}
    (h : mulSupportmulSupport f ⊆ (s : Set α)) : ∏ᶠ i, f i = ∏ i ∈ s, f i :=
  haveI h' : (s.finite_toSet.subset h).toFinset ⊆ s := by
    simpa [← Finset.coe_subset, Set.coe_toFinset]
  finprod_eq_prod_of_mulSupport_toFinset_subset _ _ h'

Finite Product Equals Finset Product When Support is Subset of Finset

Informal description

Let $f : \alpha \to M$ be a function where $M$ is a commutative monoid, and let $s$ be a finite subset of $\alpha$. If the multiplicative support of $f$ (i.e., the set $\{x \in \alpha \mid f(x) \neq 1\}$) is contained in the underlying set of $s$, then the finite product $\prodᶠ_{i} f(i)$ equals the finite product $\prod_{i \in s} f(i)$.

finprod_def theorem

 (f : α → M) [Decidable (mulSupport f).Finite] :
  ∏ᶠ i : α, f i = if h : (mulSupport f).Finite then ∏ i ∈ h.toFinset, f i else 1

Full source

@[to_additive]
theorem finprod_def (f : α → M) [Decidable (mulSupport f).Finite] :
    ∏ᶠ i : α, f i = if h : (mulSupport f).Finite then ∏ i ∈ h.toFinset, f i else 1 := by
  split_ifs with h
  · exact finprod_eq_prod_of_mulSupport_toFinset_subset _ h (Finset.Subset.refl _)
  · rw [finprod, dif_neg]
    rw [mulSupport_comp_eq_preimage]
    exact mt (fun hf => hf.of_preimage Equiv.plift.surjective) h

Definition of Finite Product via Multiplicative Support

Informal description

For a function $f : \alpha \to M$ where $M$ is a commutative monoid, the finite product $\prodᶠ_{i : \alpha} f(i)$ is defined as follows: if the multiplicative support $\{x \in \alpha \mid f(x) \neq 1\}$ is finite, then the product equals the finite product $\prod_{i \in s} f(i)$ over any finset $s$ containing the support; otherwise, the product is defined to be $1$.

finprod_of_infinite_mulSupport theorem

{f : α → M} (hf : (mulSupport f).Infinite) : ∏ᶠ i, f i = 1

Full source

@[to_additive]
theorem finprod_of_infinite_mulSupport {f : α → M} (hf : (mulSupport f).Infinite) :
    ∏ᶠ i, f i = 1 := by classical rw [finprod_def, dif_neg hf]

Finite product equals one for infinite support

Informal description

For any function $f : \alpha \to M$ where $M$ is a commutative monoid, if the multiplicative support $\{x \in \alpha \mid f(x) \neq 1\}$ is infinite, then the finite product $\prodᶠ_{i} f(i)$ equals $1$.

finprod_eq_prod theorem

(f : α → M) (hf : (mulSupport f).Finite) : ∏ᶠ i : α, f i = ∏ i ∈ hf.toFinset, f i

Full source

@[to_additive]
theorem finprod_eq_prod (f : α → M) (hf : (mulSupport f).Finite) :
    ∏ᶠ i : α, f i = ∏ i ∈ hf.toFinset, f i := by classical rw [finprod_def, dif_pos hf]

Finite product equals product over support finset

Informal description

Let $M$ be a commutative monoid and $f : \alpha \to M$ be a function with finite multiplicative support $\{x \in \alpha \mid f(x) \neq 1\}$. Then the finite product $\prodᶠ_{i \in \alpha} f(i)$ equals the finite product $\prod_{i \in s} f(i)$ over any finset $s$ containing the support of $f$.

finprod_eq_prod_of_fintype theorem

[Fintype α] (f : α → M) : ∏ᶠ i : α, f i = ∏ i, f i

Full source

@[to_additive]
theorem finprod_eq_prod_of_fintype [Fintype α] (f : α → M) : ∏ᶠ i : α, f i = ∏ i, f i :=
  finprod_eq_prod_of_mulSupport_toFinset_subset _ (Set.toFinite _) <| Finset.subset_univ _

Finite Product Equals Full Product for Finite Types

Informal description

Let $M$ be a commutative monoid and $\alpha$ be a finite type. For any function $f : \alpha \to M$, the finite product $\prodᶠ_{i : \alpha} f(i)$ equals the product $\prod_{i : \alpha} f(i)$ over all elements of $\alpha$.

map_finset_prod theorem

 {α F : Type*} [Fintype α] [EquivLike F M N] [MulEquivClass F M N] (f : F) (g : α → M) :
  f (∏ i : α, g i) = ∏ i : α, f (g i)

Full source

@[to_additive]
theorem map_finset_prod {α F : Type*} [Fintype α] [EquivLike F M N] [MulEquivClass F M N] (f : F)
    (g : α → M) : f (∏ i : α, g i) = ∏ i : α, f (g i) := by
  simp [← finprod_eq_prod_of_fintype, MulEquivClass.map_finprod]

Multiplicative Equivalence Preserves Finite Product over Finite Type

Informal description

Let $M$ and $N$ be commutative monoids, and let $F$ be a type equipped with an equivalence-like structure between $M$ and $N$ that preserves multiplication (i.e., $F$ is a `MulEquivClass`). For any finite type $\alpha$, any multiplicative equivalence $f \in F$, and any function $g \colon \alpha \to M$, we have \[ f\left(\prod_{i \in \alpha} g(i)\right) = \prod_{i \in \alpha} f(g(i)). \]

finprod_cond_eq_prod_of_cond_iff theorem

 (f : α → M) {p : α → Prop} {t : Finset α} (h : ∀ {x}, f x ≠ 1 → (p x ↔ x ∈ t)) : (∏ᶠ (i) (_ : p i), f i) = ∏ i ∈ t, f i

Full source

@[to_additive]
theorem finprod_cond_eq_prod_of_cond_iff (f : α → M) {p : α → Prop} {t : Finset α}
    (h : ∀ {x}, f x ≠ 1 → (p x ↔ x ∈ t)) : (∏ᶠ (i) (_ : p i), f i) = ∏ i ∈ t, f i := by
  set s := { x | p x }
  change ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ t, f i
  have : mulSupportmulSupport (s.mulIndicator f) ⊆ t := by
    rw [Set.mulSupport_mulIndicator]
    intro x hx
    exact (h hx.2).1 hx.1
  rw [finprod_mem_def, finprod_eq_prod_of_mulSupport_subset _ this]
  refine Finset.prod_congr rfl fun x hx => mulIndicator_apply_eq_self.2 fun hxs => ?_
  contrapose! hxs
  exact (h hxs).2 hx

Finite Product over Condition Equals Finite Product over Finite Set When Conditions Coincide on Support

Informal description

Let $M$ be a commutative monoid, $\alpha$ a type, $f : \alpha \to M$ a function, $p : \alpha \to \mathrm{Prop}$ a predicate, and $t$ a finite subset of $\alpha$. Suppose that for any $x \in \alpha$ with $f(x) \neq 1$, we have $p(x)$ if and only if $x \in t$. Then the finite product $\prodᶠ_{i \text{ with } p(i)} f(i)$ equals the finite product $\prod_{i \in t} f(i)$.

finprod_cond_ne theorem

 (f : α → M) (a : α) [DecidableEq α] (hf : (mulSupport f).Finite) :
  (∏ᶠ (i) (_ : i ≠ a), f i) = ∏ i ∈ hf.toFinset.erase a, f i

Full source

@[to_additive]
theorem finprod_cond_ne (f : α → M) (a : α) [DecidableEq α] (hf : (mulSupport f).Finite) :
    (∏ᶠ (i) (_ : i ≠ a), f i) = ∏ i ∈ hf.toFinset.erase a, f i := by
  apply finprod_cond_eq_prod_of_cond_iff
  intro x hx
  rw [Finset.mem_erase, Finite.mem_toFinset, mem_mulSupport]
  exact ⟨fun h => And.intro h hx, fun h => h.1⟩

Finite product over $i \neq a$ equals product over support minus $a$

Informal description

Let $M$ be a commutative monoid, $\alpha$ a type with decidable equality, $f : \alpha \to M$ a function with finite multiplicative support, and $a \in \alpha$. Then the finite product $\prodᶠ_{i \neq a} f(i)$ equals the finite product $\prod_{i \in t} f(i)$, where $t$ is the finite set obtained by removing $a$ from the finset representation of the multiplicative support of $f$.

finprod_mem_eq_prod_of_inter_mulSupport_eq theorem

 (f : α → M) {s : Set α} {t : Finset α} (h : s ∩ mulSupport f = t.toSet ∩ mulSupport f) : ∏ᶠ i ∈ s, f i = ∏ i ∈ t, f i

Full source

@[to_additive]
theorem finprod_mem_eq_prod_of_inter_mulSupport_eq (f : α → M) {s : Set α} {t : Finset α}
    (h : s ∩ mulSupport f = t.toSet ∩ mulSupport f) : ∏ᶠ i ∈ s, f i = ∏ i ∈ t, f i :=
  finprod_cond_eq_prod_of_cond_iff _ <| by
    intro x hxf
    rw [← mem_mulSupport] at hxf
    refine ⟨fun hx => ?_, fun hx => ?_⟩
    · refine ((mem_inter_iff x t (mulSupport f)).mp ?_).1
      rw [← Set.ext_iff.mp h x, mem_inter_iff]
      exact ⟨hx, hxf⟩
    · refine ((mem_inter_iff x s (mulSupport f)).mp ?_).1
      rw [Set.ext_iff.mp h x, mem_inter_iff]
      exact ⟨hx, hxf⟩

Finite product over a set equals finite product over a finite set when their intersections with the multiplicative support coincide

Informal description

Let $M$ be a commutative monoid, $\alpha$ a type, $f : \alpha \to M$ a function, $s \subseteq \alpha$ a subset, and $t$ a finite subset of $\alpha$. If the intersection of $s$ with the multiplicative support of $f$ equals the intersection of $t$ (viewed as a set) with the multiplicative support of $f$, then the finite product $\prodᶠ_{i \in s} f(i)$ equals the finite product $\prod_{i \in t} f(i)$.

finprod_mem_eq_prod_of_subset theorem

 (f : α → M) {s : Set α} {t : Finset α} (h₁ : s ∩ mulSupport f ⊆ t) (h₂ : ↑t ⊆ s) : ∏ᶠ i ∈ s, f i = ∏ i ∈ t, f i

Full source

@[to_additive]
theorem finprod_mem_eq_prod_of_subset (f : α → M) {s : Set α} {t : Finset α}
    (h₁ : s ∩ mulSupport fs ∩ mulSupport f ⊆ t) (h₂ : ↑t ⊆ s) : ∏ᶠ i ∈ s, f i = ∏ i ∈ t, f i :=
  finprod_cond_eq_prod_of_cond_iff _ fun hx => ⟨fun h => h₁ ⟨h, hx⟩, fun h => h₂ h⟩

Finite product over subset equals finite product over finite subset when conditions hold

Informal description

Let $M$ be a commutative monoid, $\alpha$ a type, $f : \alpha \to M$ a function, $s \subseteq \alpha$ a subset, and $t$ a finite subset of $\alpha$. If the intersection of $s$ with the multiplicative support of $f$ is contained in $t$ (i.e., $s \cap \{x \mid f(x) \neq 1\} \subseteq t$) and $t \subseteq s$, then the finite product $\prodᶠ_{i \in s} f(i)$ equals the finite product $\prod_{i \in t} f(i)$.

finprod_mem_eq_prod theorem

(f : α → M) {s : Set α} (hf : (s ∩ mulSupport f).Finite) : ∏ᶠ i ∈ s, f i = ∏ i ∈ hf.toFinset, f i

Full source

@[to_additive]
theorem finprod_mem_eq_prod (f : α → M) {s : Set α} (hf : (s ∩ mulSupport f).Finite) :
    ∏ᶠ i ∈ s, f i = ∏ i ∈ hf.toFinset, f i :=
  finprod_mem_eq_prod_of_inter_mulSupport_eq _ <| by simp [inter_assoc]

Finite product over a set equals product over its finite multiplicative support

Informal description

Let $M$ be a commutative monoid, $\alpha$ a type, $f : \alpha \to M$ a function, and $s \subseteq \alpha$ a subset. If the intersection $s \cap \{x \mid f(x) \neq 1\}$ is finite, then the finite product $\prodᶠ_{i \in s} f(i)$ equals the finite product $\prod_{i \in t} f(i)$, where $t$ is the finset corresponding to the finite set $s \cap \{x \mid f(x) \neq 1\}$.

finprod_mem_eq_prod_filter theorem

 (f : α → M) (s : Set α) [DecidablePred (· ∈ s)] (hf : (mulSupport f).Finite) :
  ∏ᶠ i ∈ s, f i = ∏ i ∈ hf.toFinset with i ∈ s, f i

Full source

@[to_additive]
theorem finprod_mem_eq_prod_filter (f : α → M) (s : Set α) [DecidablePred (· ∈ s)]
    (hf : (mulSupport f).Finite) :
    ∏ᶠ i ∈ s, f i = ∏ i ∈ hf.toFinset with i ∈ s, f i :=
  finprod_mem_eq_prod_of_inter_mulSupport_eq _ <| by
    ext x
    simp [and_comm]

Finite product over set equals filtered product over multiplicative support

Informal description

Let $M$ be a commutative monoid, $\alpha$ a type, $f : \alpha \to M$ a function, and $s \subseteq \alpha$ a subset with a decidable membership predicate. If the multiplicative support $\{x \mid f(x) \neq 1\}$ of $f$ is finite, then the finite product $\prodᶠ_{i \in s} f(i)$ equals the finite product $\prod_{i \in t} f(i)$, where $t$ is the finite subset of the multiplicative support consisting of elements that belong to $s$.

finprod_mem_eq_toFinset_prod theorem

(f : α → M) (s : Set α) [Fintype s] : ∏ᶠ i ∈ s, f i = ∏ i ∈ s.toFinset, f i

Full source

@[to_additive]
theorem finprod_mem_eq_toFinset_prod (f : α → M) (s : Set α) [Fintype s] :
    ∏ᶠ i ∈ s, f i = ∏ i ∈ s.toFinset, f i :=
  finprod_mem_eq_prod_of_inter_mulSupport_eq _ <| by simp_rw [coe_toFinset s]

Equality of Finite Product over a Finite Set and its Finite Set Representation

Informal description

Let $M$ be a commutative monoid, $\alpha$ a type, $f : \alpha \to M$ a function, and $s \subseteq \alpha$ a finite subset (with a `Fintype` instance). Then the finite product $\prodᶠ_{i \in s} f(i)$ equals the finite product $\prod_{i \in s.\mathrm{toFinset}} f(i)$, where $s.\mathrm{toFinset}$ is the finite set representation of $s$.

finprod_mem_eq_finite_toFinset_prod theorem

(f : α → M) {s : Set α} (hs : s.Finite) : ∏ᶠ i ∈ s, f i = ∏ i ∈ hs.toFinset, f i

Full source

@[to_additive]
theorem finprod_mem_eq_finite_toFinset_prod (f : α → M) {s : Set α} (hs : s.Finite) :
    ∏ᶠ i ∈ s, f i = ∏ i ∈ hs.toFinset, f i :=
  finprod_mem_eq_prod_of_inter_mulSupport_eq _ <| by rw [hs.coe_toFinset]

Finite product over a set equals product over its finset representation

Informal description

Let $M$ be a commutative monoid, $\alpha$ a type, $f : \alpha \to M$ a function, and $s \subseteq \alpha$ a finite set. Then the finite product $\prodᶠ_{i \in s} f(i)$ equals the finite product $\prod_{i \in t} f(i)$, where $t$ is the finset representation of $s$.

finprod_mem_finset_eq_prod theorem

(f : α → M) (s : Finset α) : ∏ᶠ i ∈ s, f i = ∏ i ∈ s, f i

Full source

@[to_additive]
theorem finprod_mem_finset_eq_prod (f : α → M) (s : Finset α) : ∏ᶠ i ∈ s, f i = ∏ i ∈ s, f i :=
  finprod_mem_eq_prod_of_inter_mulSupport_eq _ rfl

Equality of finite product over a finset and finset product: $\prodᶠ_{i \in s} f(i) = \prod_{i \in s} f(i)$

Informal description

For any commutative monoid $M$, any type $\alpha$, any function $f \colon \alpha \to M$, and any finite subset $s$ of $\alpha$, the finite product $\prodᶠ_{i \in s} f(i)$ equals the finite product $\prod_{i \in s} f(i)$ computed over the finset $s$.

finprod_mem_coe_finset theorem

(f : α → M) (s : Finset α) : (∏ᶠ i ∈ (s : Set α), f i) = ∏ i ∈ s, f i

Full source

@[to_additive]
theorem finprod_mem_coe_finset (f : α → M) (s : Finset α) :
    (∏ᶠ i ∈ (s : Set α), f i) = ∏ i ∈ s, f i :=
  finprod_mem_eq_prod_of_inter_mulSupport_eq _ rfl

Equality of finite product over a finset and finset product: $\prodᶠ_{i \in s} f(i) = \prod_{i \in s} f(i)$

Informal description

For any commutative monoid $M$, any type $\alpha$, any function $f \colon \alpha \to M$, and any finite subset $s$ of $\alpha$, the finite product $\prodᶠ_{i \in s} f(i)$ equals the product $\prod_{i \in s} f(i)$ computed over the finset $s$.

finprod_mem_eq_one_of_infinite theorem

{f : α → M} {s : Set α} (hs : (s ∩ mulSupport f).Infinite) : ∏ᶠ i ∈ s, f i = 1

Full source

@[to_additive]
theorem finprod_mem_eq_one_of_infinite {f : α → M} {s : Set α} (hs : (s ∩ mulSupport f).Infinite) :
    ∏ᶠ i ∈ s, f i = 1 := by
  rw [finprod_mem_def]
  apply finprod_of_infinite_mulSupport
  rwa [← mulSupport_mulIndicator] at hs

Finite product over infinite support intersection equals one

Informal description

For any function $f \colon \alpha \to M$ where $M$ is a commutative monoid, and any subset $s \subseteq \alpha$, if the intersection $s \cap \{x \in \alpha \mid f(x) \neq 1\}$ is infinite, then the finite product $\prodᶠ_{i \in s} f(i) = 1$.

finprod_mem_eq_one_of_forall_eq_one theorem

{f : α → M} {s : Set α} (h : ∀ x ∈ s, f x = 1) : ∏ᶠ i ∈ s, f i = 1

Full source

@[to_additive]
theorem finprod_mem_eq_one_of_forall_eq_one {f : α → M} {s : Set α} (h : ∀ x ∈ s, f x = 1) :
    ∏ᶠ i ∈ s, f i = 1 := by simp +contextual [h]

Finite product over a set is one when the function is identically one

Informal description

For any function $f \colon \alpha \to M$ where $M$ is a commutative monoid, and any subset $s \subseteq \alpha$, if $f(x) = 1$ for all $x \in s$, then the finite product $\prodᶠ_{i \in s} f(i) = 1$.

finprod_mem_inter_mulSupport theorem

(f : α → M) (s : Set α) : ∏ᶠ i ∈ s ∩ mulSupport f, f i = ∏ᶠ i ∈ s, f i

Full source

@[to_additive]
theorem finprod_mem_inter_mulSupport (f : α → M) (s : Set α) :
    ∏ᶠ i ∈ s ∩ mulSupport f, f i = ∏ᶠ i ∈ s, f i := by
  rw [finprod_mem_def, finprod_mem_def, mulIndicator_inter_mulSupport]

Finite Product Equality for Intersection with Multiplicative Support

Informal description

For any function $f \colon \alpha \to M$ where $M$ is a commutative monoid, and any subset $s \subseteq \alpha$, the finite product of $f$ over the intersection $s \cap \text{mulSupport}(f)$ equals the finite product of $f$ over $s$. Here, $\text{mulSupport}(f) = \{x \in \alpha \mid f(x) \neq 1\}$ is the multiplicative support of $f$. In symbols: \[ \prodᶠ_{i \in s \cap \text{mulSupport}(f)} f(i) = \prodᶠ_{i \in s} f(i). \]

finprod_mem_inter_mulSupport_eq theorem

(f : α → M) (s t : Set α) (h : s ∩ mulSupport f = t ∩ mulSupport f) : ∏ᶠ i ∈ s, f i = ∏ᶠ i ∈ t, f i

Full source

@[to_additive]
theorem finprod_mem_inter_mulSupport_eq (f : α → M) (s t : Set α)
    (h : s ∩ mulSupport f = t ∩ mulSupport f) : ∏ᶠ i ∈ s, f i = ∏ᶠ i ∈ t, f i := by
  rw [← finprod_mem_inter_mulSupport, h, finprod_mem_inter_mulSupport]

Equality of Finite Products under Equal Support Intersections

Informal description

Let $M$ be a commutative monoid and $f : \alpha \to M$ be a function. For any subsets $s, t \subseteq \alpha$, if the intersections $s \cap \text{mulSupport}(f)$ and $t \cap \text{mulSupport}(f)$ are equal, then the finite products of $f$ over $s$ and $t$ are equal, i.e., \[ \prodᶠ_{i \in s} f(i) = \prodᶠ_{i \in t} f(i). \] Here, $\text{mulSupport}(f) = \{x \in \alpha \mid f(x) \neq 1\}$ denotes the multiplicative support of $f$.

finprod_mem_inter_mulSupport_eq' theorem

 (f : α → M) (s t : Set α) (h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t) : ∏ᶠ i ∈ s, f i = ∏ᶠ i ∈ t, f i

Full source

@[to_additive]
theorem finprod_mem_inter_mulSupport_eq' (f : α → M) (s t : Set α)
    (h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t) : ∏ᶠ i ∈ s, f i = ∏ᶠ i ∈ t, f i := by
  apply finprod_mem_inter_mulSupport_eq
  ext x
  exact and_congr_left (h x)

Equality of Finite Products under Equivalent Support Conditions

Informal description

Let $M$ be a commutative monoid and $f : \alpha \to M$ be a function. For any subsets $s, t \subseteq \alpha$, if for every $x$ in the multiplicative support of $f$ (i.e., where $f(x) \neq 1$) we have $x \in s$ if and only if $x \in t$, then the finite products of $f$ over $s$ and $t$ are equal, i.e., \[ \prodᶠ_{i \in s} f(i) = \prodᶠ_{i \in t} f(i). \]

finprod_mem_univ theorem

(f : α → M) : ∏ᶠ i ∈ @Set.univ α, f i = ∏ᶠ i : α, f i

Full source

@[to_additive]
theorem finprod_mem_univ (f : α → M) : ∏ᶠ i ∈ @Set.univ α, f i = ∏ᶠ i : α, f i :=
  finprod_congr fun _ => finprod_true _

Finite Product over Universal Set Equals Global Finite Product

Informal description

For any function $f \colon \alpha \to M$ where $M$ is a commutative monoid, the finite product of $f$ over the universal set $\text{univ} = \alpha$ equals the finite product of $f$ over all elements of $\alpha$, i.e., $$\prodᶠ_{i \in \alpha} f(i) = \prodᶠ_{i : \alpha} f(i).$$

finprod_mem_congr theorem

(h₀ : s = t) (h₁ : ∀ x ∈ t, f x = g x) : ∏ᶠ i ∈ s, f i = ∏ᶠ i ∈ t, g i

Full source

@[to_additive]
theorem finprod_mem_congr (h₀ : s = t) (h₁ : ∀ x ∈ t, f x = g x) :
    ∏ᶠ i ∈ s, f i = ∏ᶠ i ∈ t, g i :=
  h₀.symm ▸ finprod_congr fun i => finprod_congr_Prop rfl (h₁ i)

Equality of Finite Products over Equal Sets with Pointwise Equal Functions

Informal description

Let $s$ and $t$ be sets in a type $\alpha$ such that $s = t$, and let $f, g : \alpha \to M$ be functions into a commutative monoid $M$. If for every $x \in t$ we have $f(x) = g(x)$, then the finite products $\prod_{i \in s} f(i)$ and $\prod_{i \in t} g(i)$ are equal.

finprod_eq_one_of_forall_eq_one theorem

{f : α → M} (h : ∀ x, f x = 1) : ∏ᶠ i, f i = 1

Full source

@[to_additive]
theorem finprod_eq_one_of_forall_eq_one {f : α → M} (h : ∀ x, f x = 1) : ∏ᶠ i, f i = 1 := by
  simp +contextual [h]

Finite product of constant one function is one

Informal description

For any function $f : \alpha \to M$ into a commutative monoid $M$, if $f(x) = 1$ for all $x \in \alpha$, then the finite product $\prodᶠ_{i \in \alpha} f(i)$ equals $1$.

one_lt_finprod' theorem

 {M : Type*} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {f : ι → M} (h : ∀ i, 1 ≤ f i)
  (h' : ∃ i, 1 < f i) (hf : (mulSupport f).Finite) : 1 < ∏ᶠ i, f i

Full source

@[to_additive finsum_pos']
theorem one_lt_finprod' {M : Type*} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M]
    {f : ι → M}
    (h : ∀ i, 1 ≤ f i) (h' : ∃ i, 1 < f i) (hf : (mulSupport f).Finite) : 1 < ∏ᶠ i, f i := by
  rcases h' with ⟨i, hi⟩
  rw [finprod_eq_prod _ hf]
  refine Finset.one_lt_prod' (fun i _ ↦ h i) ⟨i, ?_, hi⟩
  simpa only [Finite.mem_toFinset, mem_mulSupport] using ne_of_gt hi

Finite product greater than one in ordered cancellative monoids: $\prodᶠ_i f(i) > 1$ under pointwise bounds

Informal description

Let $M$ be an ordered cancellative commutative monoid and $f : \iota \to M$ a function with finite multiplicative support. If $f(i) \geq 1$ for all $i \in \iota$ and there exists some $i \in \iota$ with $f(i) > 1$, then the finite product $\prodᶠ_{i} f(i)$ is strictly greater than $1$.

finprod_mul_distrib theorem

(hf : (mulSupport f).Finite) (hg : (mulSupport g).Finite) : ∏ᶠ i, f i * g i = (∏ᶠ i, f i) * ∏ᶠ i, g i

Full source

/-- If the multiplicative supports of `f` and `g` are finite, then the product of `f i * g i` equals
the product of `f i` multiplied by the product of `g i`. -/
@[to_additive
      "If the additive supports of `f` and `g` are finite, then the sum of `f i + g i`
      equals the sum of `f i` plus the sum of `g i`."]
theorem finprod_mul_distrib (hf : (mulSupport f).Finite) (hg : (mulSupport g).Finite) :
    ∏ᶠ i, f i * g i = (∏ᶠ i, f i) * ∏ᶠ i, g i := by
  classical
    rw [finprod_eq_prod_of_mulSupport_toFinset_subset f hf Finset.subset_union_left,
      finprod_eq_prod_of_mulSupport_toFinset_subset g hg Finset.subset_union_right, ←
      Finset.prod_mul_distrib]
    refine finprod_eq_prod_of_mulSupport_subset _ ?_
    simp only [Finset.coe_union, Finite.coe_toFinset, mulSupport_subset_iff,
      mem_union, mem_mulSupport]
    intro x
    contrapose!
    rintro ⟨hf, hg⟩
    simp [hf, hg]

Distributivity of Finite Product over Multiplication: $\prodᶠ_i (f(i) \cdot g(i)) = (\prodᶠ_i f(i)) \cdot (\prodᶠ_i g(i))$

Informal description

Let $f, g : \alpha \to M$ be functions into a commutative monoid $M$. If the multiplicative supports of $f$ and $g$ (i.e., the sets $\{x \in \alpha \mid f(x) \neq 1\}$ and $\{x \in \alpha \mid g(x) \neq 1\}$) are both finite, then the finite product of $f(i) \cdot g(i)$ over all $i \in \alpha$ equals the product of the finite product of $f(i)$ and the finite product of $g(i)$. In other words: \[ \prodᶠ_{i} (f(i) \cdot g(i)) = \left(\prodᶠ_{i} f(i)\right) \cdot \left(\prodᶠ_{i} g(i)\right). \]

finprod_div_distrib theorem

 [DivisionCommMonoid G] {f g : α → G} (hf : (mulSupport f).Finite) (hg : (mulSupport g).Finite) :
  ∏ᶠ i, f i / g i = (∏ᶠ i, f i) / ∏ᶠ i, g i

Full source

/-- If the multiplicative supports of `f` and `g` are finite, then the product of `f i / g i`
equals the product of `f i` divided by the product of `g i`. -/
@[to_additive
      "If the additive supports of `f` and `g` are finite, then the sum of `f i - g i`
      equals the sum of `f i` minus the sum of `g i`."]
theorem finprod_div_distrib [DivisionCommMonoid G] {f g : α → G} (hf : (mulSupport f).Finite)
    (hg : (mulSupport g).Finite) : ∏ᶠ i, f i / g i = (∏ᶠ i, f i) / ∏ᶠ i, g i := by
  simp only [div_eq_mul_inv, finprod_mul_distrib hf ((mulSupport_inv g).symm.rec hg),
    finprod_inv_distrib]

Finite Product of Quotients Equals Quotient of Finite Products in Commutative Division Monoid

Informal description

Let $G$ be a commutative division monoid and $f, g : \alpha \to G$ be functions with finite multiplicative supports. Then the finite product of the quotients $f(i) / g(i)$ equals the quotient of the finite products of $f(i)$ and $g(i)$, i.e., \[ \prodᶠ_{i} \left(\frac{f(i)}{g(i)}\right) = \frac{\prodᶠ_{i} f(i)}{\prodᶠ_{i} g(i)}. \]

finprod_mem_mul_distrib' theorem

 (hf : (s ∩ mulSupport f).Finite) (hg : (s ∩ mulSupport g).Finite) :
  ∏ᶠ i ∈ s, f i * g i = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ s, g i

Full source

/-- A more general version of `finprod_mem_mul_distrib` that only requires `s ∩ mulSupport f` and
`s ∩ mulSupport g` rather than `s` to be finite. -/
@[to_additive
      "A more general version of `finsum_mem_add_distrib` that only requires `s ∩ support f`
      and `s ∩ support g` rather than `s` to be finite."]
theorem finprod_mem_mul_distrib' (hf : (s ∩ mulSupport f).Finite) (hg : (s ∩ mulSupport g).Finite) :
    ∏ᶠ i ∈ s, f i * g i = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ s, g i := by
  rw [← mulSupport_mulIndicator] at hf hg
  simp only [finprod_mem_def, mulIndicator_mul, finprod_mul_distrib hf hg]

Finite Product over Set Distributes over Multiplication: $\prodᶠ_{i \in s} (f(i) \cdot g(i)) = (\prodᶠ_{i \in s} f(i)) \cdot (\prodᶠ_{i \in s} g(i))$

Informal description

Let $M$ be a commutative monoid, $s$ a set in a type $\alpha$, and $f, g : \alpha \to M$ functions. If the intersections $s \cap \mathrm{mulSupport}(f)$ and $s \cap \mathrm{mulSupport}(g)$ are finite, then the finite product of $f(i) \cdot g(i)$ over $i \in s$ equals the product of the finite products of $f(i)$ and $g(i)$ over $i \in s$, i.e., \[ \prodᶠ_{i \in s} (f(i) \cdot g(i)) = \left(\prodᶠ_{i \in s} f(i)\right) \cdot \left(\prodᶠ_{i \in s} g(i)\right). \]

finprod_mem_one theorem

(s : Set α) : (∏ᶠ i ∈ s, (1 : M)) = 1

Full source

/-- The product of the constant function `1` over any set equals `1`. -/
@[to_additive "The sum of the constant function `0` over any set equals `0`."]
theorem finprod_mem_one (s : Set α) : (∏ᶠ i ∈ s, (1 : M)) = 1 := by simp

Finite Product of Constant One Function over a Set is One

Informal description

For any set $s$ in a type $\alpha$ and any commutative monoid $M$, the finite product of the constant function $1$ over the set $s$ is equal to $1$, i.e., $\prodᶠ_{i \in s} 1 = 1$.

finprod_mem_of_eqOn_one theorem

(hf : s.EqOn f 1) : ∏ᶠ i ∈ s, f i = 1

Full source

/-- If a function `f` equals `1` on a set `s`, then the product of `f i` over `i ∈ s` equals `1`. -/
@[to_additive
      "If a function `f` equals `0` on a set `s`, then the product of `f i` over `i ∈ s`
      equals `0`."]
theorem finprod_mem_of_eqOn_one (hf : s.EqOn f 1) : ∏ᶠ i ∈ s, f i = 1 := by
  rw [← finprod_mem_one s]
  exact finprod_mem_congr rfl hf

Finite Product of Function Equal to One on Set is One

Informal description

Let $M$ be a commutative monoid, $s$ a set in a type $\alpha$, and $f : \alpha \to M$ a function. If $f$ equals the constant function $1$ on $s$ (i.e., $f(x) = 1$ for all $x \in s$), then the finite product $\prod_{i \in s} f(i)$ equals $1$.

exists_ne_one_of_finprod_mem_ne_one theorem

(h : ∏ᶠ i ∈ s, f i ≠ 1) : ∃ x ∈ s, f x ≠ 1

Full source

/-- If the product of `f i` over `i ∈ s` is not equal to `1`, then there is some `x ∈ s` such that
`f x ≠ 1`. -/
@[to_additive
      "If the product of `f i` over `i ∈ s` is not equal to `0`, then there is some `x ∈ s`
      such that `f x ≠ 0`."]
theorem exists_ne_one_of_finprod_mem_ne_one (h : ∏ᶠ i ∈ s, f i∏ᶠ i ∈ s, f i ≠ 1) : ∃ x ∈ s, f x ≠ 1 := by
  by_contra! h'
  exact h (finprod_mem_of_eqOn_one h')

Existence of Non-Identity Element in Finite Product with Non-Identity Result

Informal description

Let $M$ be a commutative monoid, $s$ a set in a type $\alpha$, and $f : \alpha \to M$ a function. If the finite product $\prod_{i \in s} f(i) \neq 1$, then there exists an element $x \in s$ such that $f(x) \neq 1$.

finprod_mem_mul_distrib theorem

(hs : s.Finite) : ∏ᶠ i ∈ s, f i * g i = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ s, g i

Full source

/-- Given a finite set `s`, the product of `f i * g i` over `i ∈ s` equals the product of `f i`
over `i ∈ s` times the product of `g i` over `i ∈ s`. -/
@[to_additive
      "Given a finite set `s`, the sum of `f i + g i` over `i ∈ s` equals the sum of `f i`
      over `i ∈ s` plus the sum of `g i` over `i ∈ s`."]
theorem finprod_mem_mul_distrib (hs : s.Finite) :
    ∏ᶠ i ∈ s, f i * g i = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ s, g i :=
  finprod_mem_mul_distrib' (hs.inter_of_left _) (hs.inter_of_left _)

Finite product distributivity: $\prod_{i \in s} (f(i)g(i)) = (\prod_{i \in s} f(i))(\prod_{i \in s} g(i))$ for finite $s$

Informal description

Let $M$ be a commutative monoid, $s$ a finite set in a type $\alpha$, and $f, g : \alpha \to M$ functions. Then the finite product of $f(i) \cdot g(i)$ over $i \in s$ equals the product of the finite products of $f(i)$ and $g(i)$ over $i \in s$, i.e., \[ \prod_{i \in s} (f(i) \cdot g(i)) = \left(\prod_{i \in s} f(i)\right) \cdot \left(\prod_{i \in s} g(i)\right). \]

MonoidHom.map_finprod theorem

{f : α → M} (g : M →* N) (hf : (mulSupport f).Finite) : g (∏ᶠ i, f i) = ∏ᶠ i, g (f i)

Full source

@[to_additive]
theorem MonoidHom.map_finprod {f : α → M} (g : M →* N) (hf : (mulSupport f).Finite) :
    g (∏ᶠ i, f i) = ∏ᶠ i, g (f i) :=
  g.map_finprod_plift f <| hf.preimage Equiv.plift.injective.injOn

Monoid homomorphism preserves finite product over finite support

Informal description

Let $M$ and $N$ be commutative monoids, and let $g : M \to N$ be a monoid homomorphism. For any function $f : \alpha \to M$ with finite multiplicative support (i.e., the set $\{x \in \alpha \mid f(x) \neq 1\}$ is finite), we have \[ g\left(\prodᶠ_{i} f(i)\right) = \prodᶠ_{i} g(f(i)). \]

finprod_pow theorem

(hf : (mulSupport f).Finite) (n : ℕ) : (∏ᶠ i, f i) ^ n = ∏ᶠ i, f i ^ n

Full source

@[to_additive]
theorem finprod_pow (hf : (mulSupport f).Finite) (n : ℕ) : (∏ᶠ i, f i) ^ n = ∏ᶠ i, f i ^ n :=
  (powMonoidHom n).map_finprod hf

Power of Finite Product Equals Finite Product of Powers

Informal description

Let $M$ be a commutative monoid and $f : \alpha \to M$ be a function with finite multiplicative support (i.e., the set $\{x \in \alpha \mid f(x) \neq 1\}$ is finite). Then for any natural number $n$, the $n$-th power of the finite product of $f$ equals the finite product of the $n$-th powers of $f$: \[ \left(\prodᶠ_{i} f(i)\right)^n = \prodᶠ_{i} (f(i))^n. \]

finsum_smul' theorem

 {R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] {f : ι → R} (hf : (support f).Finite) (x : M) :
  (∑ᶠ i, f i) • x = ∑ᶠ i, f i • x

Full source

/-- See also `finsum_smul` for a version that works even when the support of `f` is not finite,
but with slightly stronger typeclass requirements. -/
theorem finsum_smul' {R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] {f : ι → R}
    (hf : (support f).Finite) (x : M) : (∑ᶠ i, f i) • x = ∑ᶠ i, f i • x :=
  ((smulAddHom R M).flip x).map_finsum hf

Finite sum commutes with scalar multiplication in modules

Informal description

Let $R$ be a semiring and $M$ an $R$-module. For any function $f : \iota \to R$ with finite support (i.e., the set $\{i \in \iota \mid f(i) \neq 0\}$ is finite) and any $x \in M$, we have \[ \left(\sumᶠ_{i} f(i)\right) \cdot x = \sumᶠ_{i} f(i) \cdot x. \]

smul_finsum' theorem

 {R M : Type*} [Monoid R] [AddCommMonoid M] [DistribMulAction R M] (c : R) {f : ι → M} (hf : (support f).Finite) :
  (c • ∑ᶠ i, f i) = ∑ᶠ i, c • f i

Full source

/-- See also `smul_finsum` for a version that works even when the support of `f` is not finite,
but with slightly stronger typeclass requirements. -/
theorem smul_finsum' {R M : Type*} [Monoid R] [AddCommMonoid M] [DistribMulAction R M] (c : R)
    {f : ι → M} (hf : (support f).Finite) : (c • ∑ᶠ i, f i) = ∑ᶠ i, c • f i :=
  (DistribMulAction.toAddMonoidHom M c).map_finsum hf

Scalar multiplication distributes over finite sums in additive commutative monoids

Informal description

Let $R$ and $M$ be types, where $R$ is a monoid and $M$ is an additive commutative monoid equipped with a distributive multiplicative action of $R$ on $M$. For any scalar $c \in R$ and any function $f : \iota \to M$ with finite support, we have the equality: \[ c \cdot \left( \sumᶠ_{i} f(i) \right) = \sumᶠ_{i} (c \cdot f(i)) \]

MonoidHom.map_finprod_mem' theorem

{f : α → M} (g : M →* N) (h₀ : (s ∩ mulSupport f).Finite) : g (∏ᶠ j ∈ s, f j) = ∏ᶠ i ∈ s, g (f i)

Full source

/-- A more general version of `MonoidHom.map_finprod_mem` that requires `s ∩ mulSupport f` rather
than `s` to be finite. -/
@[to_additive
      "A more general version of `AddMonoidHom.map_finsum_mem` that requires
      `s ∩ support f` rather than `s` to be finite."]
theorem MonoidHom.map_finprod_mem' {f : α → M} (g : M →* N) (h₀ : (s ∩ mulSupport f).Finite) :
    g (∏ᶠ j ∈ s, f j) = ∏ᶠ i ∈ s, g (f i) := by
  rw [g.map_finprod]
  · simp only [g.map_finprod_Prop]
  · simpa only [finprod_eq_mulIndicator_apply, mulSupport_mulIndicator]

Monoid homomorphism preserves finite product over intersection with multiplicative support

Informal description

Let $M$ and $N$ be commutative monoids, $g : M \to N$ a monoid homomorphism, $f : \alpha \to M$ a function, and $s \subseteq \alpha$ a subset. If the intersection $s \cap \text{mulSupport}(f)$ is finite (where $\text{mulSupport}(f) = \{x \in \alpha \mid f(x) \neq 1\}$), then \[ g\left(\prodᶠ_{j \in s} f(j)\right) = \prodᶠ_{i \in s} g(f(i)). \]

MonoidHom.map_finprod_mem theorem

(f : α → M) (g : M →* N) (hs : s.Finite) : g (∏ᶠ j ∈ s, f j) = ∏ᶠ i ∈ s, g (f i)

Full source

/-- Given a monoid homomorphism `g : M →* N` and a function `f : α → M`, the value of `g` at the
product of `f i` over `i ∈ s` equals the product of `g (f i)` over `s`. -/
@[to_additive
      "Given an additive monoid homomorphism `g : M →* N` and a function `f : α → M`, the
      value of `g` at the sum of `f i` over `i ∈ s` equals the sum of `g (f i)` over `s`."]
theorem MonoidHom.map_finprod_mem (f : α → M) (g : M →* N) (hs : s.Finite) :
    g (∏ᶠ j ∈ s, f j) = ∏ᶠ i ∈ s, g (f i) :=
  g.map_finprod_mem' (hs.inter_of_left _)

Monoid Homomorphism Preserves Finite Product over Finite Set

Informal description

Let $M$ and $N$ be commutative monoids, $g : M \to N$ a monoid homomorphism, $f : \alpha \to M$ a function, and $s \subseteq \alpha$ a finite subset. Then \[ g\left(\prodᶠ_{j \in s} f(j)\right) = \prodᶠ_{i \in s} g(f(i)). \]

MulEquiv.map_finprod_mem theorem

(g : M ≃* N) (f : α → M) {s : Set α} (hs : s.Finite) : g (∏ᶠ i ∈ s, f i) = ∏ᶠ i ∈ s, g (f i)

Full source

@[to_additive]
theorem MulEquiv.map_finprod_mem (g : M ≃* N) (f : α → M) {s : Set α} (hs : s.Finite) :
    g (∏ᶠ i ∈ s, f i) = ∏ᶠ i ∈ s, g (f i) :=
  g.toMonoidHom.map_finprod_mem f hs

Multiplicative Isomorphism Preserves Finite Product over Finite Set

Informal description

Let $M$ and $N$ be commutative monoids, $g \colon M \simeq^* N$ a multiplicative equivalence (isomorphism), $f \colon \alpha \to M$ a function, and $s \subseteq \alpha$ a finite subset. Then \[ g\left(\prodᶠ_{i \in s} f(i)\right) = \prodᶠ_{i \in s} g(f(i)). \]

finprod_mem_inv_distrib theorem

[DivisionCommMonoid G] (f : α → G) (hs : s.Finite) : (∏ᶠ x ∈ s, (f x)⁻¹) = (∏ᶠ x ∈ s, f x)⁻¹

Full source

@[to_additive]
theorem finprod_mem_inv_distrib [DivisionCommMonoid G] (f : α → G) (hs : s.Finite) :
    (∏ᶠ x ∈ s, (f x)⁻¹) = (∏ᶠ x ∈ s, f x)⁻¹ :=
  ((MulEquiv.inv G).map_finprod_mem f hs).symm

Inverse of Finite Product Equals Finite Product of Inverses in Commutative Division Monoid

Informal description

Let $G$ be a commutative division monoid, $f : \alpha \to G$ a function, and $s \subseteq \alpha$ a finite subset. Then the finite product of the inverses of $f(x)$ over $x \in s$ is equal to the inverse of the finite product of $f(x)$ over $x \in s$, i.e., \[ \prod_{x \in s} (f(x))^{-1} = \left(\prod_{x \in s} f(x)\right)^{-1}. \]

finprod_mem_div_distrib theorem

 [DivisionCommMonoid G] (f g : α → G) (hs : s.Finite) : ∏ᶠ i ∈ s, f i / g i = (∏ᶠ i ∈ s, f i) / ∏ᶠ i ∈ s, g i

Full source

/-- Given a finite set `s`, the product of `f i / g i` over `i ∈ s` equals the product of `f i`
over `i ∈ s` divided by the product of `g i` over `i ∈ s`. -/
@[to_additive
      "Given a finite set `s`, the sum of `f i / g i` over `i ∈ s` equals the sum of `f i`
      over `i ∈ s` minus the sum of `g i` over `i ∈ s`."]
theorem finprod_mem_div_distrib [DivisionCommMonoid G] (f g : α → G) (hs : s.Finite) :
    ∏ᶠ i ∈ s, f i / g i = (∏ᶠ i ∈ s, f i) / ∏ᶠ i ∈ s, g i := by
  simp only [div_eq_mul_inv, finprod_mem_mul_distrib hs, finprod_mem_inv_distrib g hs]

Finite Product of Quotients Equals Quotient of Finite Products in Commutative Division Monoid

Informal description

Let $G$ be a commutative division monoid, $f, g : \alpha \to G$ functions, and $s \subseteq \alpha$ a finite subset. Then the finite product of the quotients $f(i)/g(i)$ over $i \in s$ equals the quotient of the finite products of $f(i)$ and $g(i)$ over $i \in s$, i.e., \[ \prod_{i \in s} \frac{f(i)}{g(i)} = \frac{\prod_{i \in s} f(i)}{\prod_{i \in s} g(i)}. \]

finprod_mem_empty theorem

: (∏ᶠ i ∈ (∅ : Set α), f i) = 1

Full source

/-- The product of any function over an empty set is `1`. -/
@[to_additive "The sum of any function over an empty set is `0`."]
theorem finprod_mem_empty : (∏ᶠ i ∈ (∅ : Set α), f i) = 1 := by simp

Finite Product over Empty Set is One

Informal description

For any function $f : \alpha \to M$ where $M$ is a commutative monoid, the finite product over the empty set is equal to the multiplicative identity, i.e., $\prodᶠ_{i \in \emptyset} f(i) = 1$.

nonempty_of_finprod_mem_ne_one theorem

(h : ∏ᶠ i ∈ s, f i ≠ 1) : s.Nonempty

Full source

/-- A set `s` is nonempty if the product of some function over `s` is not equal to `1`. -/
@[to_additive "A set `s` is nonempty if the sum of some function over `s` is not equal to `0`."]
theorem nonempty_of_finprod_mem_ne_one (h : ∏ᶠ i ∈ s, f i∏ᶠ i ∈ s, f i ≠ 1) : s.Nonempty :=
  nonempty_iff_ne_empty.2 fun h' => h <| h'.symm ▸ finprod_mem_empty

Nonemptiness from Non-trivial Finite Product

Informal description

For any function $f : \alpha \to M$ where $M$ is a commutative monoid, if the finite product $\prodᶠ_{i \in s} f(i)$ over a set $s$ is not equal to the multiplicative identity $1$, then the set $s$ is nonempty.

finprod_mem_union_inter theorem

 (hs : s.Finite) (ht : t.Finite) : ((∏ᶠ i ∈ s ∪ t, f i) * ∏ᶠ i ∈ s ∩ t, f i) = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t, f i

Full source

/-- Given finite sets `s` and `t`, the product of `f i` over `i ∈ s ∪ t` times the product of
`f i` over `i ∈ s ∩ t` equals the product of `f i` over `i ∈ s` times the product of `f i`
over `i ∈ t`. -/
@[to_additive
      "Given finite sets `s` and `t`, the sum of `f i` over `i ∈ s ∪ t` plus the sum of
      `f i` over `i ∈ s ∩ t` equals the sum of `f i` over `i ∈ s` plus the sum of `f i`
      over `i ∈ t`."]
theorem finprod_mem_union_inter (hs : s.Finite) (ht : t.Finite) :
    ((∏ᶠ i ∈ s ∪ t, f i) * ∏ᶠ i ∈ s ∩ t, f i) = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t, f i := by
  lift s to Finset α using hs; lift t to Finset α using ht
  classical
    rw [← Finset.coe_union, ← Finset.coe_inter]
    simp only [finprod_mem_coe_finset, Finset.prod_union_inter]

Product over Union and Intersection: $\prod_{s \cup t} f \cdot \prod_{s \cap t} f = \prod_s f \cdot \prod_t f$

Informal description

For any commutative monoid $M$, any function $f : \alpha \to M$, and any finite sets $s, t \subseteq \alpha$, the following identity holds: \[ \left(\prod_{i \in s \cup t} f(i)\right) \cdot \left(\prod_{i \in s \cap t} f(i)\right) = \left(\prod_{i \in s} f(i)\right) \cdot \left(\prod_{i \in t} f(i)\right). \]

finprod_mem_union_inter' theorem

 (hs : (s ∩ mulSupport f).Finite) (ht : (t ∩ mulSupport f).Finite) :
  ((∏ᶠ i ∈ s ∪ t, f i) * ∏ᶠ i ∈ s ∩ t, f i) = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t, f i

Full source

/-- A more general version of `finprod_mem_union_inter` that requires `s ∩ mulSupport f` and
`t ∩ mulSupport f` rather than `s` and `t` to be finite. -/
@[to_additive
      "A more general version of `finsum_mem_union_inter` that requires `s ∩ support f` and
      `t ∩ support f` rather than `s` and `t` to be finite."]
theorem finprod_mem_union_inter' (hs : (s ∩ mulSupport f).Finite) (ht : (t ∩ mulSupport f).Finite) :
    ((∏ᶠ i ∈ s ∪ t, f i) * ∏ᶠ i ∈ s ∩ t, f i) = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t, f i := by
  rw [← finprod_mem_inter_mulSupport f s, ← finprod_mem_inter_mulSupport f t, ←
    finprod_mem_union_inter hs ht, ← union_inter_distrib_right, finprod_mem_inter_mulSupport, ←
    finprod_mem_inter_mulSupport f (s ∩ t)]
  congr 2
  rw [inter_left_comm, inter_assoc, inter_assoc, inter_self, inter_left_comm]

Generalized product identity over union and intersection with multiplicative support

Informal description

Let $M$ be a commutative monoid and $f : \alpha \to M$ a function. For any sets $s, t \subseteq \alpha$ such that $s \cap \text{mulSupport}(f)$ and $t \cap \text{mulSupport}(f)$ are finite, the following identity holds: \[ \left(\prodᶠ_{i \in s \cup t} f(i)\right) \cdot \left(\prodᶠ_{i \in s \cap t} f(i)\right) = \left(\prodᶠ_{i \in s} f(i)\right) \cdot \left(\prodᶠ_{i \in t} f(i)\right), \] where $\text{mulSupport}(f) = \{x \in \alpha \mid f(x) \neq 1\}$ is the multiplicative support of $f$.

finprod_mem_union' theorem

 (hst : Disjoint s t) (hs : (s ∩ mulSupport f).Finite) (ht : (t ∩ mulSupport f).Finite) :
  ∏ᶠ i ∈ s ∪ t, f i = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t, f i

Full source

/-- A more general version of `finprod_mem_union` that requires `s ∩ mulSupport f` and
`t ∩ mulSupport f` rather than `s` and `t` to be finite. -/
@[to_additive
      "A more general version of `finsum_mem_union` that requires `s ∩ support f` and
      `t ∩ support f` rather than `s` and `t` to be finite."]
theorem finprod_mem_union' (hst : Disjoint s t) (hs : (s ∩ mulSupport f).Finite)
    (ht : (t ∩ mulSupport f).Finite) : ∏ᶠ i ∈ s ∪ t, f i = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t, f i := by
  rw [← finprod_mem_union_inter' hs ht, disjoint_iff_inter_eq_empty.1 hst, finprod_mem_empty,
    mul_one]

Finite product over disjoint union with multiplicative support condition

Informal description

Let $M$ be a commutative monoid and $f : \alpha \to M$ a function. For any disjoint sets $s, t \subseteq \alpha$ such that $s \cap \text{mulSupport}(f)$ and $t \cap \text{mulSupport}(f)$ are finite, the finite product of $f$ over the union $s \cup t$ satisfies: \[ \prodᶠ_{i \in s \cup t} f(i) = \left(\prodᶠ_{i \in s} f(i)\right) \cdot \left(\prodᶠ_{i \in t} f(i)\right), \] where $\text{mulSupport}(f) = \{x \in \alpha \mid f(x) \neq 1\}$ is the multiplicative support of $f$.

finprod_mem_union theorem

 (hst : Disjoint s t) (hs : s.Finite) (ht : t.Finite) : ∏ᶠ i ∈ s ∪ t, f i = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t, f i

Full source

/-- Given two finite disjoint sets `s` and `t`, the product of `f i` over `i ∈ s ∪ t` equals the
product of `f i` over `i ∈ s` times the product of `f i` over `i ∈ t`. -/
@[to_additive
      "Given two finite disjoint sets `s` and `t`, the sum of `f i` over `i ∈ s ∪ t` equals
      the sum of `f i` over `i ∈ s` plus the sum of `f i` over `i ∈ t`."]
theorem finprod_mem_union (hst : Disjoint s t) (hs : s.Finite) (ht : t.Finite) :
    ∏ᶠ i ∈ s ∪ t, f i = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t, f i :=
  finprod_mem_union' hst (hs.inter_of_left _) (ht.inter_of_left _)

Finite product over disjoint union of finite sets

Informal description

Let $M$ be a commutative monoid and $f : \alpha \to M$ a function. For any finite disjoint sets $s, t \subseteq \alpha$, the finite product of $f$ over the union $s \cup t$ satisfies: \[ \prodᶠ_{i \in s \cup t} f(i) = \left(\prodᶠ_{i \in s} f(i)\right) \cdot \left(\prodᶠ_{i \in t} f(i)\right). \]

finprod_mem_union'' theorem

 (hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)) (hs : (s ∩ mulSupport f).Finite)
  (ht : (t ∩ mulSupport f).Finite) : ∏ᶠ i ∈ s ∪ t, f i = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t, f i

Full source

/-- A more general version of `finprod_mem_union'` that requires `s ∩ mulSupport f` and
`t ∩ mulSupport f` rather than `s` and `t` to be disjoint -/
@[to_additive
      "A more general version of `finsum_mem_union'` that requires `s ∩ support f` and
      `t ∩ support f` rather than `s` and `t` to be disjoint"]
theorem finprod_mem_union'' (hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f))
    (hs : (s ∩ mulSupport f).Finite) (ht : (t ∩ mulSupport f).Finite) :
    ∏ᶠ i ∈ s ∪ t, f i = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t, f i := by
  rw [← finprod_mem_inter_mulSupport f s, ← finprod_mem_inter_mulSupport f t, ←
    finprod_mem_union hst hs ht, ← union_inter_distrib_right, finprod_mem_inter_mulSupport]

Finite Product over Union with Disjoint Multiplicative Supports

Informal description

Let $M$ be a commutative monoid and $f : \alpha \to M$ a function. For any sets $s, t \subseteq \alpha$ such that: 1. The intersections $s \cap \text{mulSupport}(f)$ and $t \cap \text{mulSupport}(f)$ are disjoint, where $\text{mulSupport}(f) = \{x \in \alpha \mid f(x) \neq 1\}$ is the multiplicative support of $f$; 2. Both $s \cap \text{mulSupport}(f)$ and $t \cap \text{mulSupport}(f)$ are finite; then the finite product of $f$ over the union $s \cup t$ satisfies: \[ \prodᶠ_{i \in s \cup t} f(i) = \left(\prodᶠ_{i \in s} f(i)\right) \cdot \left(\prodᶠ_{i \in t} f(i)\right). \]

finprod_mem_singleton theorem

: (∏ᶠ i ∈ ({ a } : Set α), f i) = f a

Full source

/-- The product of `f i` over `i ∈ {a}` equals `f a`. -/
@[to_additive "The sum of `f i` over `i ∈ {a}` equals `f a`."]
theorem finprod_mem_singleton : (∏ᶠ i ∈ ({a} : Set α), f i) = f a := by
  rw [← Finset.coe_singleton, finprod_mem_coe_finset, Finset.prod_singleton]

Finite Product over Singleton: $\prodᶠ_{i \in \{a\}} f(i) = f(a)$

Informal description

For any commutative monoid $M$, any type $\alpha$, any element $a \in \alpha$, and any function $f \colon \alpha \to M$, the finite product of $f(i)$ over the singleton set $\{a\}$ equals $f(a)$, i.e., $$\prodᶠ_{i \in \{a\}} f(i) = f(a).$$

finprod_cond_eq_left theorem

: (∏ᶠ (i) (_ : i = a), f i) = f a

Full source

@[to_additive (attr := simp)]
theorem finprod_cond_eq_left : (∏ᶠ (i) (_ : i = a), f i) = f a :=
  finprod_mem_singleton

Finite Product over Equality Condition: $\prodᶠ_{i = a} f(i) = f(a)$

Informal description

For any commutative monoid $M$, any type $\alpha$, any element $a \in \alpha$, and any function $f \colon \alpha \to M$, the finite product of $f(i)$ over all $i$ satisfying $i = a$ equals $f(a)$, i.e., $$\prodᶠ_{i = a} f(i) = f(a).$$

finprod_cond_eq_right theorem

: (∏ᶠ (i) (_ : a = i), f i) = f a

Full source

@[to_additive (attr := simp)]
theorem finprod_cond_eq_right : (∏ᶠ (i) (_ : a = i), f i) = f a := by simp [@eq_comm _ a]

Finite Product over Reverse Equality Condition: $\prodᶠ_{a = i} f(i) = f(a)$

Informal description

For any commutative monoid $M$, any type $\alpha$, any element $a \in \alpha$, and any function $f \colon \alpha \to M$, the finite product of $f(i)$ over all $i$ satisfying $a = i$ equals $f(a)$, i.e., $$\prodᶠ_{a = i} f(i) = f(a).$$

finprod_mem_insert' theorem

 (f : α → M) (h : a ∉ s) (hs : (s ∩ mulSupport f).Finite) : ∏ᶠ i ∈ insert a s, f i = f a * ∏ᶠ i ∈ s, f i

Full source

/-- A more general version of `finprod_mem_insert` that requires `s ∩ mulSupport f` rather than `s`
to be finite. -/
@[to_additive
      "A more general version of `finsum_mem_insert` that requires `s ∩ support f` rather
      than `s` to be finite."]
theorem finprod_mem_insert' (f : α → M) (h : a ∉ s) (hs : (s ∩ mulSupport f).Finite) :
    ∏ᶠ i ∈ insert a s, f i = f a * ∏ᶠ i ∈ s, f i := by
  rw [insert_eq, finprod_mem_union' _ _ hs, finprod_mem_singleton]
  · rwa [disjoint_singleton_left]
  · exact (finite_singleton a).inter_of_left _

Finite product over insertion with multiplicative support condition: $\prodᶠ_{i \in \{a\} \cup s} f(i) = f(a) \cdot \prodᶠ_{i \in s} f(i)$

Informal description

Let $M$ be a commutative monoid, $f : \alpha \to M$ a function, $s \subseteq \alpha$ a subset, and $a \in \alpha$ an element such that $a \notin s$. If the intersection $s \cap \text{mulSupport}(f)$ is finite, where $\text{mulSupport}(f) = \{x \in \alpha \mid f(x) \neq 1\}$, then the finite product of $f$ over the set $\{a\} \cup s$ satisfies: \[ \prodᶠ_{i \in \{a\} \cup s} f(i) = f(a) \cdot \left(\prodᶠ_{i \in s} f(i)\right). \]

finprod_mem_insert theorem

(f : α → M) (h : a ∉ s) (hs : s.Finite) : ∏ᶠ i ∈ insert a s, f i = f a * ∏ᶠ i ∈ s, f i

Full source

/-- Given a finite set `s` and an element `a ∉ s`, the product of `f i` over `i ∈ insert a s` equals
`f a` times the product of `f i` over `i ∈ s`. -/
@[to_additive
      "Given a finite set `s` and an element `a ∉ s`, the sum of `f i` over `i ∈ insert a s`
      equals `f a` plus the sum of `f i` over `i ∈ s`."]
theorem finprod_mem_insert (f : α → M) (h : a ∉ s) (hs : s.Finite) :
    ∏ᶠ i ∈ insert a s, f i = f a * ∏ᶠ i ∈ s, f i :=
  finprod_mem_insert' f h <| hs.inter_of_left _

Finite product decomposition over insertion: $\prodᶠ_{i \in \{a\} \cup s} f(i) = f(a) \cdot \prodᶠ_{i \in s} f(i)$

Informal description

Let $M$ be a commutative monoid, $f : \alpha \to M$ a function, $s \subseteq \alpha$ a finite subset, and $a \in \alpha$ an element such that $a \notin s$. Then the finite product of $f$ over the set $\{a\} \cup s$ satisfies: \[ \prodᶠ_{i \in \{a\} \cup s} f(i) = f(a) \cdot \left(\prodᶠ_{i \in s} f(i)\right). \]

finprod_mem_insert_of_eq_one_if_not_mem theorem

(h : a ∉ s → f a = 1) : ∏ᶠ i ∈ insert a s, f i = ∏ᶠ i ∈ s, f i

Full source

/-- If `f a = 1` when `a ∉ s`, then the product of `f i` over `i ∈ insert a s` equals the product of
`f i` over `i ∈ s`. -/
@[to_additive
      "If `f a = 0` when `a ∉ s`, then the sum of `f i` over `i ∈ insert a s` equals the sum
      of `f i` over `i ∈ s`."]
theorem finprod_mem_insert_of_eq_one_if_not_mem (h : a ∉ s → f a = 1) :
    ∏ᶠ i ∈ insert a s, f i = ∏ᶠ i ∈ s, f i := by
  refine finprod_mem_inter_mulSupport_eq' _ _ _ fun x hx => ⟨?_, Or.inr⟩
  rintro (rfl | hxs)
  exacts [not_imp_comm.1 h hx, hxs]

Finite Product over Inserted Set when Function Vanishes Outside

Informal description

Let $M$ be a commutative monoid, $f : \alpha \to M$ a function, $s \subseteq \alpha$ a subset, and $a \in \alpha$ an element. If $f(a) = 1$ whenever $a \notin s$, then the finite product of $f$ over the set $\{a\} \cup s$ equals the finite product of $f$ over $s$, i.e., \[ \prodᶠ_{i \in \{a\} \cup s} f(i) = \prodᶠ_{i \in s} f(i). \]

finprod_mem_insert_one theorem

(h : f a = 1) : ∏ᶠ i ∈ insert a s, f i = ∏ᶠ i ∈ s, f i

Full source

/-- If `f a = 1`, then the product of `f i` over `i ∈ insert a s` equals the product of `f i` over
`i ∈ s`. -/
@[to_additive
      "If `f a = 0`, then the sum of `f i` over `i ∈ insert a s` equals the sum of `f i`
      over `i ∈ s`."]
theorem finprod_mem_insert_one (h : f a = 1) : ∏ᶠ i ∈ insert a s, f i = ∏ᶠ i ∈ s, f i :=
  finprod_mem_insert_of_eq_one_if_not_mem fun _ => h

Finite Product over Inserted Set with Unit Value

Informal description

Let $M$ be a commutative monoid, $f : \alpha \to M$ a function, $s \subseteq \alpha$ a subset, and $a \in \alpha$ an element. If $f(a) = 1$, then the finite product of $f$ over the set $\{a\} \cup s$ equals the finite product of $f$ over $s$, i.e., \[ \prodᶠ_{i \in \{a\} \cup s} f(i) = \prodᶠ_{i \in s} f(i). \]

finprod_mem_dvd theorem

{f : α → N} (a : α) (hf : (mulSupport f).Finite) : f a ∣ finprod f

Full source

/-- If the multiplicative support of `f` is finite, then for every `x` in the domain of `f`, `f x`
divides `finprod f`. -/
theorem finprod_mem_dvd {f : α → N} (a : α) (hf : (mulSupport f).Finite) : f a ∣ finprod f := by
  by_cases ha : a ∈ mulSupport f
  · rw [finprod_eq_prod_of_mulSupport_toFinset_subset f hf (Set.Subset.refl _)]
    exact Finset.dvd_prod_of_mem f ((Finite.mem_toFinset hf).mpr ha)
  · rw [nmem_mulSupport.mp ha]
    exact one_dvd (finprod f)

Divisibility of Finite Product by Function Values

Informal description

Let $f : \alpha \to N$ be a function into a commutative monoid $N$, and suppose the multiplicative support of $f$ (i.e., the set $\{x \in \alpha \mid f(x) \neq 1\}$) is finite. Then for any $a \in \alpha$, the value $f(a)$ divides the finite product $\prodᶠ_{i} f(i)$.

finprod_mem_pair theorem

(h : a ≠ b) : (∏ᶠ i ∈ ({ a, b } : Set α), f i) = f a * f b

Full source

/-- The product of `f i` over `i ∈ {a, b}`, `a ≠ b`, is equal to `f a * f b`. -/
@[to_additive "The sum of `f i` over `i ∈ {a, b}`, `a ≠ b`, is equal to `f a + f b`."]
theorem finprod_mem_pair (h : a ≠ b) : (∏ᶠ i ∈ ({a, b} : Set α), f i) = f a * f b := by
  rw [finprod_mem_insert, finprod_mem_singleton]
  exacts [h, finite_singleton b]

Finite Product over Doubleton: $\prodᶠ_{i \in \{a, b\}} f(i) = f(a) \cdot f(b)$

Informal description

For any commutative monoid $M$, any type $\alpha$, any two distinct elements $a, b \in \alpha$, and any function $f \colon \alpha \to M$, the finite product of $f(i)$ over the doubleton set $\{a, b\}$ equals $f(a) \cdot f(b)$, i.e., $$\prodᶠ_{i \in \{a, b\}} f(i) = f(a) \cdot f(b).$$

finprod_mem_image' theorem

 {s : Set β} {g : β → α} (hg : (s ∩ mulSupport (f ∘ g)).InjOn g) : ∏ᶠ i ∈ g '' s, f i = ∏ᶠ j ∈ s, f (g j)

Full source

/-- The product of `f y` over `y ∈ g '' s` equals the product of `f (g i)` over `s`
provided that `g` is injective on `s ∩ mulSupport (f ∘ g)`. -/
@[to_additive
      "The sum of `f y` over `y ∈ g '' s` equals the sum of `f (g i)` over `s` provided that
      `g` is injective on `s ∩ support (f ∘ g)`."]
theorem finprod_mem_image' {s : Set β} {g : β → α} (hg : (s ∩ mulSupport (f ∘ g)).InjOn g) :
    ∏ᶠ i ∈ g '' s, f i = ∏ᶠ j ∈ s, f (g j) := by
  classical
    by_cases hs : (s ∩ mulSupport (f ∘ g)).Finite
    · have hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y := by
        simpa only [hs.mem_toFinset]
      have := finprod_mem_eq_prod (comp f g) hs
      unfold Function.comp at this
      rw [this, ← Finset.prod_image hg]
      refine finprod_mem_eq_prod_of_inter_mulSupport_eq f ?_
      rw [Finset.coe_image, hs.coe_toFinset, ← image_inter_mulSupport_eq, inter_assoc, inter_self]
    · unfold Function.comp at hs
      rw [finprod_mem_eq_one_of_infinite hs, finprod_mem_eq_one_of_infinite]
      rwa [image_inter_mulSupport_eq, infinite_image_iff hg]

Finite product over image equals finite product over source under injectivity condition

Informal description

Let $M$ be a commutative monoid, $\alpha$ and $\beta$ types, $f : \alpha \to M$ a function, $s \subseteq \beta$ a subset, and $g : \beta \to \alpha$ a function that is injective on $s \cap \{y \in \beta \mid f(g(y)) \neq 1\}$. Then the finite product $\prodᶠ_{i \in g(s)} f(i)$ equals the finite product $\prodᶠ_{j \in s} f(g(j))$.

finprod_mem_image theorem

{s : Set β} {g : β → α} (hg : s.InjOn g) : ∏ᶠ i ∈ g '' s, f i = ∏ᶠ j ∈ s, f (g j)

Full source

/-- The product of `f y` over `y ∈ g '' s` equals the product of `f (g i)` over `s` provided that
`g` is injective on `s`. -/
@[to_additive
      "The sum of `f y` over `y ∈ g '' s` equals the sum of `f (g i)` over `s` provided that
      `g` is injective on `s`."]
theorem finprod_mem_image {s : Set β} {g : β → α} (hg : s.InjOn g) :
    ∏ᶠ i ∈ g '' s, f i = ∏ᶠ j ∈ s, f (g j) :=
  finprod_mem_image' <| hg.mono inter_subset_left

Finite product over image equals finite product over source under injectivity

Informal description

Let $M$ be a commutative monoid, $\alpha$ and $\beta$ types, $f : \alpha \to M$ a function, $s \subseteq \beta$ a subset, and $g : \beta \to \alpha$ a function that is injective on $s$. Then the finite product of $f$ over the image $g(s)$ equals the finite product of $f \circ g$ over $s$, i.e., $$\prodᶠ_{i \in g(s)} f(i) = \prodᶠ_{j \in s} f(g(j)).$$

finprod_mem_range' theorem

{g : β → α} (hg : (mulSupport (f ∘ g)).InjOn g) : ∏ᶠ i ∈ range g, f i = ∏ᶠ j, f (g j)

Full source

/-- The product of `f y` over `y ∈ Set.range g` equals the product of `f (g i)` over all `i`
provided that `g` is injective on `mulSupport (f ∘ g)`. -/
@[to_additive
      "The sum of `f y` over `y ∈ Set.range g` equals the sum of `f (g i)` over all `i`
      provided that `g` is injective on `support (f ∘ g)`."]
theorem finprod_mem_range' {g : β → α} (hg : (mulSupport (f ∘ g)).InjOn g) :
    ∏ᶠ i ∈ range g, f i = ∏ᶠ j, f (g j) := by
  rw [← image_univ, finprod_mem_image', finprod_mem_univ]
  rwa [univ_inter]

Finite Product over Range Equals Finite Product over Source under Injectivity on Support

Informal description

Let $M$ be a commutative monoid, $\alpha$ and $\beta$ types, $f : \alpha \to M$ a function, and $g : \beta \to \alpha$ a function that is injective on the multiplicative support of $f \circ g$ (i.e., the set $\{y \in \beta \mid f(g(y)) \neq 1\}$). Then the finite product of $f$ over the range of $g$ equals the finite product of $f \circ g$ over all elements of $\beta$, i.e., $$\prodᶠ_{i \in \text{range}(g)} f(i) = \prodᶠ_{j \in \beta} f(g(j)).$$

finprod_mem_range theorem

{g : β → α} (hg : Injective g) : ∏ᶠ i ∈ range g, f i = ∏ᶠ j, f (g j)

Full source

/-- The product of `f y` over `y ∈ Set.range g` equals the product of `f (g i)` over all `i`
provided that `g` is injective. -/
@[to_additive
      "The sum of `f y` over `y ∈ Set.range g` equals the sum of `f (g i)` over all `i`
      provided that `g` is injective."]
theorem finprod_mem_range {g : β → α} (hg : Injective g) : ∏ᶠ i ∈ range g, f i = ∏ᶠ j, f (g j) :=
  finprod_mem_range' hg.injOn

Finite Product over Range Equals Finite Product over Source for Injective Functions

Informal description

Let $M$ be a commutative monoid, $\alpha$ and $\beta$ types, $f : \alpha \to M$ a function, and $g : \beta \to \alpha$ an injective function. Then the finite product of $f$ over the range of $g$ equals the finite product of $f \circ g$ over all elements of $\beta$, i.e., $$\prodᶠ_{i \in \text{range}(g)} f(i) = \prodᶠ_{j \in \beta} f(g(j)).$$

finprod_mem_eq_of_bijOn theorem

 {s : Set α} {t : Set β} {f : α → M} {g : β → M} (e : α → β) (he₀ : s.BijOn e t) (he₁ : ∀ x ∈ s, f x = g (e x)) :
  ∏ᶠ i ∈ s, f i = ∏ᶠ j ∈ t, g j

Full source

/-- See also `Finset.prod_bij`. -/
@[to_additive "See also `Finset.sum_bij`."]
theorem finprod_mem_eq_of_bijOn {s : Set α} {t : Set β} {f : α → M} {g : β → M} (e : α → β)
    (he₀ : s.BijOn e t) (he₁ : ∀ x ∈ s, f x = g (e x)) : ∏ᶠ i ∈ s, f i = ∏ᶠ j ∈ t, g j := by
  rw [← Set.BijOn.image_eq he₀, finprod_mem_image he₀.2.1]
  exact finprod_mem_congr rfl he₁

Equality of Finite Products under Bijection

Informal description

Let $M$ be a commutative monoid, $\alpha$ and $\beta$ types, $s \subseteq \alpha$ and $t \subseteq \beta$ subsets, and $f : \alpha \to M$, $g : \beta \to M$ functions. Given a bijection $e : \alpha \to \beta$ that restricts to a bijection from $s$ to $t$ (i.e., $e$ is injective on $s$, maps $s$ into $t$, and $e(s) = t$), and satisfies $f(x) = g(e(x))$ for all $x \in s$, then the finite products $\prod_{i \in s} f(i)$ and $\prod_{j \in t} g(j)$ are equal.

finprod_eq_of_bijective theorem

 {f : α → M} {g : β → M} (e : α → β) (he₀ : Bijective e) (he₁ : ∀ x, f x = g (e x)) : ∏ᶠ i, f i = ∏ᶠ j, g j

Full source

/-- See `finprod_comp`, `Fintype.prod_bijective` and `Finset.prod_bij`. -/
@[to_additive "See `finsum_comp`, `Fintype.sum_bijective` and `Finset.sum_bij`."]
theorem finprod_eq_of_bijective {f : α → M} {g : β → M} (e : α → β) (he₀ : Bijective e)
    (he₁ : ∀ x, f x = g (e x)) : ∏ᶠ i, f i = ∏ᶠ j, g j := by
  rw [← finprod_mem_univ f, ← finprod_mem_univ g]
  exact finprod_mem_eq_of_bijOn _ (bijective_iff_bijOn_univ.mp he₀) fun x _ => he₁ x

Equality of Finite Products under Bijective Change of Variables

Informal description

Let $M$ be a commutative monoid, and let $f \colon \alpha \to M$ and $g \colon \beta \to M$ be functions. Given a bijective function $e \colon \alpha \to \beta$ such that $f(x) = g(e(x))$ for all $x \in \alpha$, then the finite products $\prod_{i \in \alpha} f(i)$ and $\prod_{j \in \beta} g(j)$ are equal.

finprod_comp theorem

{g : β → M} (e : α → β) (he₀ : Function.Bijective e) : (∏ᶠ i, g (e i)) = ∏ᶠ j, g j

Full source

/-- See also `finprod_eq_of_bijective`, `Fintype.prod_bijective` and `Finset.prod_bij`. -/
@[to_additive "See also `finsum_eq_of_bijective`, `Fintype.sum_bijective` and `Finset.sum_bij`."]
theorem finprod_comp {g : β → M} (e : α → β) (he₀ : Function.Bijective e) :
    (∏ᶠ i, g (e i)) = ∏ᶠ j, g j :=
  finprod_eq_of_bijective e he₀ fun _ => rfl

Finite Product Invariance under Bijective Reindexing: $\prod_{i} g(e(i)) = \prod_{j} g(j)$

Informal description

Let $M$ be a commutative monoid, $g \colon \beta \to M$ a function, and $e \colon \alpha \to \beta$ a bijective function. Then the finite product $\prod_{i \in \alpha} g(e(i))$ is equal to the finite product $\prod_{j \in \beta} g(j)$.

finprod_comp_equiv theorem

(e : α ≃ β) {f : β → M} : (∏ᶠ i, f (e i)) = ∏ᶠ i', f i'

Full source

@[to_additive]
theorem finprod_comp_equiv (e : α ≃ β) {f : β → M} : (∏ᶠ i, f (e i)) = ∏ᶠ i', f i' :=
  finprod_comp e e.bijective

Finite Product Invariance under Equivalence: $\prod_{i} f(e(i)) = \prod_{i'} f(i')$

Informal description

Let $M$ be a commutative monoid, $\alpha$ and $\beta$ be types, and $e : \alpha \simeq \beta$ be an equivalence (bijection) between them. For any function $f : \beta \to M$, the finite product $\prod_{i \in \alpha} f(e(i))$ is equal to the finite product $\prod_{i' \in \beta} f(i')$.

finprod_set_coe_eq_finprod_mem theorem

(s : Set α) : ∏ᶠ j : s, f j = ∏ᶠ i ∈ s, f i

Full source

@[to_additive]
theorem finprod_set_coe_eq_finprod_mem (s : Set α) : ∏ᶠ j : s, f j = ∏ᶠ i ∈ s, f i := by
  rw [← finprod_mem_range, Subtype.range_coe]
  exact Subtype.coe_injective

Equality of Finite Products over Subtype and Set Elements

Informal description

For any set $s$ in a type $\alpha$ and any function $f : \alpha \to M$ where $M$ is a commutative monoid, the finite product of $f$ over the elements of the subtype corresponding to $s$ is equal to the finite product of $f$ over the elements of $s$, i.e., $$\prodᶠ_{j \in s} f(j) = \prodᶠ_{i \in s} f(i).$$

finprod_subtype_eq_finprod_cond theorem

(p : α → Prop) : ∏ᶠ j : Subtype p, f j = ∏ᶠ (i) (_ : p i), f i

Full source

@[to_additive]
theorem finprod_subtype_eq_finprod_cond (p : α → Prop) :
    ∏ᶠ j : Subtype p, f j = ∏ᶠ (i) (_ : p i), f i :=
  finprod_set_coe_eq_finprod_mem { i | p i }

Finite Product over Subtype Equals Finite Product over Condition

Informal description

For any predicate $p : \alpha \to \text{Prop}$ and any function $f : \alpha \to M$ where $M$ is a commutative monoid, the finite product of $f$ over the subtype defined by $p$ is equal to the finite product of $f$ over all elements $i$ satisfying $p(i)$, i.e., \[ \prodᶠ_{j \in \{x \mid p x\}} f(j) = \prodᶠ_{i \text{ s.t. } p i} f(i). \]

finprod_mem_inter_mul_diff' theorem

 (t : Set α) (h : (s ∩ mulSupport f).Finite) : ((∏ᶠ i ∈ s ∩ t, f i) * ∏ᶠ i ∈ s \ t, f i) = ∏ᶠ i ∈ s, f i

Full source

@[to_additive]
theorem finprod_mem_inter_mul_diff' (t : Set α) (h : (s ∩ mulSupport f).Finite) :
    ((∏ᶠ i ∈ s ∩ t, f i) * ∏ᶠ i ∈ s \ t, f i) = ∏ᶠ i ∈ s, f i := by
  rw [← finprod_mem_union', inter_union_diff]
  · rw [disjoint_iff_inf_le]
    exact fun x hx => hx.2.2 hx.1.2
  exacts [h.subset fun x hx => ⟨hx.1.1, hx.2⟩, h.subset fun x hx => ⟨hx.1.1, hx.2⟩]

Decomposition of Finite Product over Intersection and Difference: $\prodᶠ_{s \cap t} f \cdot \prodᶠ_{s \setminus t} f = \prodᶠ_s f$

Informal description

Let $M$ be a commutative monoid and $f : \alpha \to M$ a function. For any set $s \subseteq \alpha$ such that $s \cap \text{mulSupport}(f)$ is finite, and for any subset $t \subseteq \alpha$, the following equality holds: \[ \left(\prodᶠ_{i \in s \cap t} f(i)\right) \cdot \left(\prodᶠ_{i \in s \setminus t} f(i)\right) = \prodᶠ_{i \in s} f(i), \] where $\text{mulSupport}(f) = \{x \in \alpha \mid f(x) \neq 1\}$ is the multiplicative support of $f$.

finprod_mem_inter_mul_diff theorem

(t : Set α) (h : s.Finite) : ((∏ᶠ i ∈ s ∩ t, f i) * ∏ᶠ i ∈ s \ t, f i) = ∏ᶠ i ∈ s, f i

Full source

@[to_additive]
theorem finprod_mem_inter_mul_diff (t : Set α) (h : s.Finite) :
    ((∏ᶠ i ∈ s ∩ t, f i) * ∏ᶠ i ∈ s \ t, f i) = ∏ᶠ i ∈ s, f i :=
  finprod_mem_inter_mul_diff' _ <| h.inter_of_left _

Decomposition of finite product over intersection and difference: $\prodᶠ_{s \cap t} f \cdot \prodᶠ_{s \setminus t} f = \prodᶠ_s f$ for finite $s$

Informal description

Let $M$ be a commutative monoid and $f : \alpha \to M$ a function. For any finite subset $s \subseteq \alpha$ and any subset $t \subseteq \alpha$, the following equality holds: \[ \left(\prodᶠ_{i \in s \cap t} f(i)\right) \cdot \left(\prodᶠ_{i \in s \setminus t} f(i)\right) = \prodᶠ_{i \in s} f(i), \] where $\prodᶠ$ denotes the finite product over the specified set.

finprod_mem_mul_diff' theorem

 (hst : s ⊆ t) (ht : (t ∩ mulSupport f).Finite) : ((∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t \ s, f i) = ∏ᶠ i ∈ t, f i

Full source

/-- A more general version of `finprod_mem_mul_diff` that requires `t ∩ mulSupport f` rather than
`t` to be finite. -/
@[to_additive
      "A more general version of `finsum_mem_add_diff` that requires `t ∩ support f` rather
      than `t` to be finite."]
theorem finprod_mem_mul_diff' (hst : s ⊆ t) (ht : (t ∩ mulSupport f).Finite) :
    ((∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t \ s, f i) = ∏ᶠ i ∈ t, f i := by
  rw [← finprod_mem_inter_mul_diff' _ ht, inter_eq_self_of_subset_right hst]

Decomposition of Finite Product over Subset and Complement: $\prodᶠ_s f \cdot \prodᶠ_{t \setminus s} f = \prodᶠ_t f$

Informal description

Let $M$ be a commutative monoid and $f : \alpha \to M$ a function. For any subsets $s \subseteq t \subseteq \alpha$ such that $t \cap \text{mulSupport}(f)$ is finite, the following equality holds: \[ \left(\prodᶠ_{i \in s} f(i)\right) \cdot \left(\prodᶠ_{i \in t \setminus s} f(i)\right) = \prodᶠ_{i \in t} f(i), \] where $\text{mulSupport}(f) = \{x \in \alpha \mid f(x) \neq 1\}$ is the multiplicative support of $f$.

finprod_mem_mul_diff theorem

(hst : s ⊆ t) (ht : t.Finite) : ((∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t \ s, f i) = ∏ᶠ i ∈ t, f i

Full source

/-- Given a finite set `t` and a subset `s` of `t`, the product of `f i` over `i ∈ s`
times the product of `f i` over `t \ s` equals the product of `f i` over `i ∈ t`. -/
@[to_additive
      "Given a finite set `t` and a subset `s` of `t`, the sum of `f i` over `i ∈ s` plus
      the sum of `f i` over `t \\ s` equals the sum of `f i` over `i ∈ t`."]
theorem finprod_mem_mul_diff (hst : s ⊆ t) (ht : t.Finite) :
    ((∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t \ s, f i) = ∏ᶠ i ∈ t, f i :=
  finprod_mem_mul_diff' hst (ht.inter_of_left _)

Product Decomposition over Subset and Complement: $\prod_s f \cdot \prod_{t \setminus s} f = \prod_t f$ for finite $t$

Informal description

Let $M$ be a commutative monoid and $f : \alpha \to M$ a function. For any finite subset $t \subseteq \alpha$ and any subset $s \subseteq t$, the following equality holds: \[ \left(\prod_{i \in s} f(i)\right) \cdot \left(\prod_{i \in t \setminus s} f(i)\right) = \prod_{i \in t} f(i), \] where $\prod$ denotes the finite product over the specified set.

finprod_mem_iUnion theorem

 [Finite ι] {t : ι → Set α} (h : Pairwise (Disjoint on t)) (ht : ∀ i, (t i).Finite) :
  ∏ᶠ a ∈ ⋃ i : ι, t i, f a = ∏ᶠ i, ∏ᶠ a ∈ t i, f a

Full source

/-- Given a family of pairwise disjoint finite sets `t i` indexed by a finite type, the product of
`f a` over the union `⋃ i, t i` is equal to the product over all indexes `i` of the products of
`f a` over `a ∈ t i`. -/
@[to_additive
      "Given a family of pairwise disjoint finite sets `t i` indexed by a finite type, the
      sum of `f a` over the union `⋃ i, t i` is equal to the sum over all indexes `i` of the
      sums of `f a` over `a ∈ t i`."]
theorem finprod_mem_iUnion [Finite ι] {t : ι → Set α} (h : Pairwise (DisjointDisjoint on t))
    (ht : ∀ i, (t i).Finite) : ∏ᶠ a ∈ ⋃ i : ι, t i, f a = ∏ᶠ i, ∏ᶠ a ∈ t i, f a := by
  cases nonempty_fintype ι
  lift t to ι → Finset α using ht
  classical
    rw [← biUnion_univ, ← Finset.coe_univ, ← Finset.coe_biUnion, finprod_mem_coe_finset,
      Finset.prod_biUnion]
    · simp only [finprod_mem_coe_finset, finprod_eq_prod_of_fintype]
    · exact fun x _ y _ hxy => Finset.disjoint_coe.1 (h hxy)

Product over Union of Pairwise Disjoint Finite Sets

Informal description

Let $\iota$ be a finite type, and let $\{t_i\}_{i \in \iota}$ be a family of pairwise disjoint finite subsets of a type $\alpha$. For any function $f : \alpha \to M$ where $M$ is a commutative monoid, the product of $f(a)$ over all $a$ in the union $\bigcup_{i \in \iota} t_i$ is equal to the product over all indices $i \in \iota$ of the products of $f(a)$ over all $a \in t_i$. In symbols: \[ \prod_{a \in \bigcup_{i \in \iota} t_i} f(a) = \prod_{i \in \iota} \prod_{a \in t_i} f(a). \]

finprod_mem_biUnion theorem

 {I : Set ι} {t : ι → Set α} (h : I.PairwiseDisjoint t) (hI : I.Finite) (ht : ∀ i ∈ I, (t i).Finite) :
  ∏ᶠ a ∈ ⋃ x ∈ I, t x, f a = ∏ᶠ i ∈ I, ∏ᶠ j ∈ t i, f j

Full source

/-- Given a family of sets `t : ι → Set α`, a finite set `I` in the index type such that all sets
`t i`, `i ∈ I`, are finite, if all `t i`, `i ∈ I`, are pairwise disjoint, then the product of `f a`
over `a ∈ ⋃ i ∈ I, t i` is equal to the product over `i ∈ I` of the products of `f a` over
`a ∈ t i`. -/
@[to_additive
      "Given a family of sets `t : ι → Set α`, a finite set `I` in the index type such that
      all sets `t i`, `i ∈ I`, are finite, if all `t i`, `i ∈ I`, are pairwise disjoint, then the
      sum of `f a` over `a ∈ ⋃ i ∈ I, t i` is equal to the sum over `i ∈ I` of the sums of `f a`
      over `a ∈ t i`."]
theorem finprod_mem_biUnion {I : Set ι} {t : ι → Set α} (h : I.PairwiseDisjoint t) (hI : I.Finite)
    (ht : ∀ i ∈ I, (t i).Finite) : ∏ᶠ a ∈ ⋃ x ∈ I, t x, f a = ∏ᶠ i ∈ I, ∏ᶠ j ∈ t i, f j := by
  haveI := hI.fintype
  rw [biUnion_eq_iUnion, finprod_mem_iUnion, ← finprod_set_coe_eq_finprod_mem]
  exacts [fun x y hxy => h x.2 y.2 (Subtype.coe_injective.ne hxy), fun b => ht b b.2]

Product over Union of Pairwise Disjoint Finite Sets via Bounded Union

Informal description

Let $I$ be a finite set of indices, and let $\{t_i\}_{i \in I}$ be a family of finite subsets of a type $\alpha$ such that the $t_i$ are pairwise disjoint for $i \in I$. For any function $f : \alpha \to M$, where $M$ is a commutative monoid, the product of $f(a)$ over all $a$ in the union $\bigcup_{i \in I} t_i$ is equal to the product over $i \in I$ of the products of $f(j)$ over all $j \in t_i$. In symbols: \[ \prod_{a \in \bigcup_{i \in I} t_i} f(a) = \prod_{i \in I} \prod_{j \in t_i} f(j). \]

finprod_mem_sUnion theorem

 {t : Set (Set α)} (h : t.PairwiseDisjoint id) (ht₀ : t.Finite) (ht₁ : ∀ x ∈ t, Set.Finite x) :
  ∏ᶠ a ∈ ⋃₀ t, f a = ∏ᶠ s ∈ t, ∏ᶠ a ∈ s, f a

Full source

/-- If `t` is a finite set of pairwise disjoint finite sets, then the product of `f a`
over `a ∈ ⋃₀ t` is the product over `s ∈ t` of the products of `f a` over `a ∈ s`. -/
@[to_additive
      "If `t` is a finite set of pairwise disjoint finite sets, then the sum of `f a` over
      `a ∈ ⋃₀ t` is the sum over `s ∈ t` of the sums of `f a` over `a ∈ s`."]
theorem finprod_mem_sUnion {t : Set (Set α)} (h : t.PairwiseDisjoint id) (ht₀ : t.Finite)
    (ht₁ : ∀ x ∈ t, Set.Finite x) : ∏ᶠ a ∈ ⋃₀ t, f a = ∏ᶠ s ∈ t, ∏ᶠ a ∈ s, f a := by
  rw [Set.sUnion_eq_biUnion]
  exact finprod_mem_biUnion h ht₀ ht₁

Product over Union of Pairwise Disjoint Finite Sets: $\prod_{a \in \bigcup_{s \in t} s} f(a) = \prod_{s \in t} \prod_{a \in s} f(a)$

Informal description

Let $t$ be a finite family of finite subsets of a type $\alpha$ such that the sets in $t$ are pairwise disjoint. For any function $f : \alpha \to M$, where $M$ is a commutative monoid, the product of $f(a)$ over all $a$ in the union $\bigcup_{s \in t} s$ is equal to the product over $s \in t$ of the products of $f(a)$ over all $a \in s$. In symbols: \[ \prod_{a \in \bigcup_{s \in t} s} f(a) = \prod_{s \in t} \prod_{a \in s} f(a). \]

finprod_option theorem

{f : Option α → M} (hf : (mulSupport (f ∘ some)).Finite) : ∏ᶠ o, f o = f none * ∏ᶠ a, f (some a)

Full source

@[to_additive]
lemma finprod_option {f : Option α → M} (hf : (mulSupport (f ∘ some)).Finite) :
    ∏ᶠ o, f o = f none * ∏ᶠ a, f (some a) := by
  replace hf : (mulSupport f).Finite := by simpa [finite_option]
  convert finprod_mem_insert' f (show nonenone ∉ Set.range Option.some by aesop)
    (hf.subset inter_subset_right)
  · aesop
  · rw [finprod_mem_range]
    exact Option.some_injective _

Finite product over Option type: $\prodᶠ_{o} f(o) = f(\text{none}) \cdot \prodᶠ_{a} f(\text{some}(a))$

Informal description

Let $M$ be a commutative monoid and $f : \text{Option}\ \alpha \to M$ a function such that the multiplicative support of $f \circ \text{some}$ is finite. Then the finite product of $f$ over all elements of $\text{Option}\ \alpha$ equals the product of $f(\text{none})$ with the finite product of $f(\text{some}(a))$ over all $a \in \alpha$. That is, \[ \prodᶠ_{o \in \text{Option}\ \alpha} f(o) = f(\text{none}) \cdot \left( \prodᶠ_{a \in \alpha} f(\text{some}(a)) \right). \]

mul_finprod_cond_ne theorem

(a : α) (hf : (mulSupport f).Finite) : (f a * ∏ᶠ (i) (_ : i ≠ a), f i) = ∏ᶠ i, f i

Full source

@[to_additive]
theorem mul_finprod_cond_ne (a : α) (hf : (mulSupport f).Finite) :
    (f a * ∏ᶠ (i) (_ : i ≠ a), f i) = ∏ᶠ i, f i := by
  classical
    rw [finprod_eq_prod _ hf]
    have h : ∀ x : α, f x ≠ 1 → (x ≠ ax ≠ a ↔ x ∈ hf.toFinset \ {a}) := by
      intro x hx
      rw [Finset.mem_sdiff, Finset.mem_singleton, Finite.mem_toFinset, mem_mulSupport]
      exact ⟨fun h => And.intro hx h, fun h => h.2⟩
    rw [finprod_cond_eq_prod_of_cond_iff f (fun hx => h _ hx), Finset.sdiff_singleton_eq_erase]
    by_cases ha : a ∈ mulSupport f
    · apply Finset.mul_prod_erase _ _ ((Finite.mem_toFinset _).mpr ha)
    · rw [mem_mulSupport, not_not] at ha
      rw [ha, one_mul]
      apply Finset.prod_erase _ ha

Factorization of Finite Product via Exclusion: $f(a) \cdot \prodᶠ_{i \neq a} f(i) = \prodᶠ_i f(i)$

Informal description

Let $M$ be a commutative monoid, $\alpha$ a type, and $f : \alpha \to M$ a function with finite multiplicative support. For any element $a \in \alpha$, the product of $f(a)$ with the finite product of $f(i)$ over all $i \neq a$ equals the finite product of $f(i)$ over all $i \in \alpha$. That is, \[ f(a) \cdot \left( \prodᶠ_{\substack{i \in \alpha \\ i \neq a}} f(i) \right) = \prodᶠ_{i \in \alpha} f(i). \]

finprod_mem_comm theorem

 {s : Set α} {t : Set β} (f : α → β → M) (hs : s.Finite) (ht : t.Finite) :
  (∏ᶠ i ∈ s, ∏ᶠ j ∈ t, f i j) = ∏ᶠ j ∈ t, ∏ᶠ i ∈ s, f i j

Full source

/-- If `s : Set α` and `t : Set β` are finite sets, then taking the product over `s` commutes with
taking the product over `t`. -/
@[to_additive
      "If `s : Set α` and `t : Set β` are finite sets, then summing over `s` commutes with
      summing over `t`."]
theorem finprod_mem_comm {s : Set α} {t : Set β} (f : α → β → M) (hs : s.Finite) (ht : t.Finite) :
    (∏ᶠ i ∈ s, ∏ᶠ j ∈ t, f i j) = ∏ᶠ j ∈ t, ∏ᶠ i ∈ s, f i j := by
  lift s to Finset α using hs; lift t to Finset β using ht
  simp only [finprod_mem_coe_finset]
  exact Finset.prod_comm

Commutativity of Finite Products over Finite Sets: $\prod_{i \in s} \prod_{j \in t} f(i,j) = \prod_{j \in t} \prod_{i \in s} f(i,j)$

Informal description

Let $M$ be a commutative monoid, $s \subseteq \alpha$ and $t \subseteq \beta$ be finite sets, and $f : \alpha \to \beta \to M$ be a function. Then the finite product over $s$ of the finite products over $t$ of $f(i,j)$ equals the finite product over $t$ of the finite products over $s$ of $f(i,j)$. In other words: \[ \prod_{i \in s} \left( \prod_{j \in t} f(i,j) \right) = \prod_{j \in t} \left( \prod_{i \in s} f(i,j) \right). \]

finprod_mem_induction theorem

 (p : M → Prop) (hp₀ : p 1) (hp₁ : ∀ x y, p x → p y → p (x * y)) (hp₂ : ∀ x ∈ s, p <| f x) : p (∏ᶠ i ∈ s, f i)

Full source

/-- To prove a property of a finite product, it suffices to prove that the property is
multiplicative and holds on factors. -/
@[to_additive
      "To prove a property of a finite sum, it suffices to prove that the property is
      additive and holds on summands."]
theorem finprod_mem_induction (p : M → Prop) (hp₀ : p 1) (hp₁ : ∀ x y, p x → p y → p (x * y))
    (hp₂ : ∀ x ∈ s, p <| f x) : p (∏ᶠ i ∈ s, f i) :=
  finprod_induction _ hp₀ hp₁ fun x => finprod_induction _ hp₀ hp₁ <| hp₂ x

Induction Principle for Finite Products over Sets in Commutative Monoids

Informal description

Let $M$ be a commutative monoid, $s$ a set in type $\alpha$, and $f : \alpha \to M$ a function. For any predicate $p : M \to \mathrm{Prop}$ satisfying: 1. $p(1)$ holds, 2. $p$ is multiplicative (i.e., $p(x)$ and $p(y)$ imply $p(x \cdot y)$ for all $x, y \in M$), 3. $p(f(x))$ holds for all $x \in s$, then $p\left(\prodᶠ_{i \in s} f(i)\right)$ holds, where $\prodᶠ_{i \in s}$ denotes the finite product over the set $s$.

finprod_cond_nonneg theorem

 {R : Type*} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] {p : α → Prop} {f : α → R} (hf : ∀ x, p x → 0 ≤ f x) :
  0 ≤ ∏ᶠ (x) (_ : p x), f x

Full source

theorem finprod_cond_nonneg {R : Type*} [CommSemiring R] [PartialOrder R] [IsOrderedRing R]
    {p : α → Prop} {f : α → R}
    (hf : ∀ x, p x → 0 ≤ f x) : 0 ≤ ∏ᶠ (x) (_ : p x), f x :=
  finprod_nonneg fun x => finprod_nonneg <| hf x

Nonnegativity of Conditional Finite Products in Ordered Semirings

Informal description

Let $R$ be a commutative semiring with a partial order $\leq$ and the structure of an ordered ring. For any predicate $p : \alpha \to \mathrm{Prop}$ and function $f : \alpha \to R$ such that $f(x) \geq 0$ for all $x$ satisfying $p(x)$, the finite product $\prodᶠ_{x \mid p(x)} f(x)$ is nonnegative, i.e., $0 \leq \prodᶠ_{x \mid p(x)} f(x)$.

single_le_finprod theorem

 {M : Type*} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] (i : α) {f : α → M} (hf : (mulSupport f).Finite)
  (h : ∀ j, 1 ≤ f j) : f i ≤ ∏ᶠ j, f j

Full source

@[to_additive]
theorem single_le_finprod {M : Type*} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M]
    (i : α) {f : α → M}
    (hf : (mulSupport f).Finite) (h : ∀ j, 1 ≤ f j) : f i ≤ ∏ᶠ j, f j := by
  classical calc
      f i ≤ ∏ j ∈ insert i hf.toFinset, f j :=
        Finset.single_le_prod' (fun j _ => h j) (Finset.mem_insert_self _ _)
      _ = ∏ᶠ j, f j :=
        (finprod_eq_prod_of_mulSupport_toFinset_subset _ hf (Finset.subset_insert _ _)).symm

Element Bounded by Finite Product in Ordered Commutative Monoid

Informal description

Let $M$ be a partially ordered commutative monoid where the multiplication is order-preserving. For any function $f : \alpha \to M$ with finite multiplicative support (i.e., $\{x \in \alpha \mid f(x) \neq 1\}$ is finite) and any index $i \in \alpha$, if $1 \leq f(j)$ for all $j \in \alpha$, then $f(i) \leq \prodᶠ_{j} f(j)$.

finprod_eq_zero theorem

 {M₀ : Type*} [CommMonoidWithZero M₀] (f : α → M₀) (x : α) (hx : f x = 0) (hf : (mulSupport f).Finite) : ∏ᶠ x, f x = 0

Full source

theorem finprod_eq_zero {M₀ : Type*} [CommMonoidWithZero M₀] (f : α → M₀) (x : α) (hx : f x = 0)
    (hf : (mulSupport f).Finite) : ∏ᶠ x, f x = 0 := by
  nontriviality
  rw [finprod_eq_prod f hf]
  refine Finset.prod_eq_zero (hf.mem_toFinset.2 ?_) hx
  simp [hx]

Finite Product Vanishes at Zero

Informal description

Let $M₀$ be a commutative monoid with zero. For any function $f : \alpha \to M₀$ with finite multiplicative support, if there exists $x \in \alpha$ such that $f(x) = 0$, then the finite product $\prodᶠ_{x} f(x)$ equals zero.

finprod_prod_comm theorem

 (s : Finset β) (f : α → β → M) (h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite) :
  (∏ᶠ a : α, ∏ b ∈ s, f a b) = ∏ b ∈ s, ∏ᶠ a : α, f a b

Full source

@[to_additive]
theorem finprod_prod_comm (s : Finset β) (f : α → β → M)
    (h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite) :
    (∏ᶠ a : α, ∏ b ∈ s, f a b) = ∏ b ∈ s, ∏ᶠ a : α, f a b := by
  have hU :
    (mulSupport fun a => ∏ b ∈ s, f a b) ⊆
      (s.finite_toSet.biUnion fun b hb => h b (Finset.mem_coe.1 hb)).toFinset := by
    rw [Finite.coe_toFinset]
    intro x hx
    simp only [exists_prop, mem_iUnion, Ne, mem_mulSupport, Finset.mem_coe]
    contrapose! hx
    rw [mem_mulSupport, not_not, Finset.prod_congr rfl hx, Finset.prod_const_one]
  rw [finprod_eq_prod_of_mulSupport_subset _ hU, Finset.prod_comm]
  refine Finset.prod_congr rfl fun b hb => (finprod_eq_prod_of_mulSupport_subset _ ?_).symm
  intro a ha
  simp only [Finite.coe_toFinset, mem_iUnion]
  exact ⟨b, hb, ha⟩

Commutativity of Finite Product and Finset Product

Informal description

Let $M$ be a commutative monoid, $s$ a finite subset of $\beta$, and $f : \alpha \to \beta \to M$ a function such that for each $b \in s$, the multiplicative support of $f(\cdot, b)$ is finite. Then the finite product over $\alpha$ of the product over $s$ of $f(a, b)$ equals the product over $s$ of the finite product over $\alpha$ of $f(a, b)$. In symbols: $$ \prodᶠ_{a \in \alpha} \prod_{b \in s} f(a, b) = \prod_{b \in s} \prodᶠ_{a \in \alpha} f(a, b). $$

prod_finprod_comm theorem

 (s : Finset α) (f : α → β → M) (h : ∀ a ∈ s, (mulSupport (f a)).Finite) :
  (∏ a ∈ s, ∏ᶠ b : β, f a b) = ∏ᶠ b : β, ∏ a ∈ s, f a b

Full source

@[to_additive]
theorem prod_finprod_comm (s : Finset α) (f : α → β → M) (h : ∀ a ∈ s, (mulSupport (f a)).Finite) :
    (∏ a ∈ s, ∏ᶠ b : β, f a b) = ∏ᶠ b : β, ∏ a ∈ s, f a b :=
  (finprod_prod_comm s (fun b a => f a b) h).symm

Commutativity of Finset Product and Finite Product

Informal description

Let $M$ be a commutative monoid, $s$ a finite subset of $\alpha$, and $f : \alpha \to \beta \to M$ a function such that for each $a \in s$, the multiplicative support of $f(a, \cdot)$ is finite. Then the product over $s$ of the finite product over $\beta$ of $f(a, b)$ equals the finite product over $\beta$ of the product over $s$ of $f(a, b)$. In symbols: $$ \prod_{a \in s} \prodᶠ_{b \in \beta} f(a, b) = \prodᶠ_{b \in \beta} \prod_{a \in s} f(a, b). $$

mul_finsum theorem

 {R : Type*} [NonUnitalNonAssocSemiring R] (f : α → R) (r : R) (h : (support f).Finite) :
  (r * ∑ᶠ a : α, f a) = ∑ᶠ a : α, r * f a

Full source

theorem mul_finsum {R : Type*} [NonUnitalNonAssocSemiring R] (f : α → R) (r : R)
    (h : (support f).Finite) : (r * ∑ᶠ a : α, f a) = ∑ᶠ a : α, r * f a :=
  (AddMonoidHom.mulLeft r).map_finsum h

Left multiplication distributes over finite sum in non-unital non-associative semiring

Informal description

Let $R$ be a non-unital, non-associative semiring, $f : \alpha \to R$ a function with finite support, and $r \in R$ an element. Then the left multiplication of $r$ with the finite sum of $f$ equals the finite sum of $r$ multiplied by $f$: $$ r \cdot \left( \sumᶠ_{a \in \alpha} f(a) \right) = \sumᶠ_{a \in \alpha} r \cdot f(a). $$

mul_finsum_mem theorem

 {R : Type*} [NonUnitalNonAssocSemiring R] {s : Set α} (f : α → R) (r : R) (hs : s.Finite) :
  (r * ∑ᶠ a ∈ s, f a) = ∑ᶠ a ∈ s, r * f a

Full source

theorem mul_finsum_mem {R : Type*} [NonUnitalNonAssocSemiring R] {s : Set α} (f : α → R) (r : R)
    (hs : s.Finite) : (r * ∑ᶠ a ∈ s, f a) = ∑ᶠ a ∈ s, r * f a :=
  (AddMonoidHom.mulLeft r).map_finsum_mem f hs

Left multiplication distributes over finite sum over a finite set in a non-unital non-associative semiring

Informal description

Let $R$ be a non-unital, non-associative semiring, $s$ a finite subset of $\alpha$, and $f : \alpha \to R$ a function. Then for any $r \in R$, the product of $r$ with the finite sum of $f$ over $s$ equals the finite sum over $s$ of $r$ multiplied by $f$: $$ r \cdot \left( \sum_{a \in s} f(a) \right) = \sum_{a \in s} r \cdot f(a). $$

finsum_mul theorem

 {R : Type*} [NonUnitalNonAssocSemiring R] (f : α → R) (r : R) (h : (support f).Finite) :
  (∑ᶠ a : α, f a) * r = ∑ᶠ a : α, f a * r

Full source

theorem finsum_mul {R : Type*} [NonUnitalNonAssocSemiring R] (f : α → R) (r : R)
    (h : (support f).Finite) : (∑ᶠ a : α, f a) * r = ∑ᶠ a : α, f a * r :=
  (AddMonoidHom.mulRight r).map_finsum h

Right Distributivity of Finite Sum over Multiplication in Non-Unital Non-Associative Semirings

Informal description

Let $R$ be a non-unital, non-associative semiring, and let $f : \alpha \to R$ be a function with finite support. Then for any $r \in R$, the product of the finite sum $\sumᶠ_{a \in \alpha} f(a)$ with $r$ is equal to the finite sum $\sumᶠ_{a \in \alpha} (f(a) * r)$.

finsum_mem_mul theorem

 {R : Type*} [NonUnitalNonAssocSemiring R] {s : Set α} (f : α → R) (r : R) (hs : s.Finite) :
  (∑ᶠ a ∈ s, f a) * r = ∑ᶠ a ∈ s, f a * r

Full source

theorem finsum_mem_mul {R : Type*} [NonUnitalNonAssocSemiring R] {s : Set α} (f : α → R) (r : R)
    (hs : s.Finite) : (∑ᶠ a ∈ s, f a) * r = ∑ᶠ a ∈ s, f a * r :=
  (AddMonoidHom.mulRight r).map_finsum_mem f hs

Right Distributivity of Finite Sum over Multiplication for Finite Sets

Informal description

Let $R$ be a non-unital, non-associative semiring, $s$ be a finite subset of a type $\alpha$, and $f \colon \alpha \to R$ be a function. Then for any $r \in R$, the product of the finite sum $\sum_{a \in s} f(a)$ with $r$ is equal to the finite sum $\sum_{a \in s} (f(a) \cdot r)$.

finprod_apply theorem

{α ι : Type*} {f : ι → α → N} (hf : (mulSupport f).Finite) (a : α) : (∏ᶠ i, f i) a = ∏ᶠ i, f i a

Full source

@[to_additive (attr := simp)]
lemma finprod_apply {α ι : Type*} {f : ι → α → N} (hf : (mulSupport f).Finite) (a : α) :
    (∏ᶠ i, f i) a = ∏ᶠ i, f i a := by
  classical
  have hf' : (mulSupport fun i ↦ f i a).Finite := hf.subset (by aesop)
  simp only [finprod_def, dif_pos, hf, hf', Finset.prod_apply]
  symm
  apply Finset.prod_subset <;> aesop

Evaluation of Finite Product of Functions: $(\prodᶠ_i f(i))(a) = \prodᶠ_i f(i)(a)$

Informal description

Let $\alpha$ and $\iota$ be types, and let $f \colon \iota \to \alpha \to N$ be a function into a commutative monoid $N$. If the multiplicative support of $f$ (i.e., the set of $i \in \iota$ such that $f(i) \neq 1$) is finite, then for any fixed $a \in \alpha$, the evaluation at $a$ of the finite product $\prodᶠ_{i} f(i)$ equals the finite product $\prodᶠ_{i} f(i)(a)$ of the evaluations.

Finset.mulSupport_of_fiberwise_prod_subset_image theorem

 [DecidableEq β] (s : Finset α) (f : α → M) (g : α → β) : (mulSupport fun b => ∏ a ∈ s with g a = b, f a) ⊆ s.image g

Full source

@[to_additive]
theorem Finset.mulSupport_of_fiberwise_prod_subset_image [DecidableEq β] (s : Finset α) (f : α → M)
    (g : α → β) : (mulSupport fun b => ∏ a ∈ s with g a = b, f a) ⊆ s.image g := by
  simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, Function.support_subset_iff]
  intro b h
  suffices {a ∈ s | g a = b}.Nonempty by
    simpa only [fiber_nonempty_iff_mem_image, Finset.mem_image, exists_prop]
  exact Finset.nonempty_of_prod_ne_one h

Multiplicative Support of Fiberwise Product is Subset of Image under $g$

Informal description

Let $\alpha$ and $\beta$ be types with decidable equality, $s$ be a finite subset of $\alpha$, $f : \alpha \to M$ be a function into a commutative monoid $M$, and $g : \alpha \to \beta$ be a function. Then the multiplicative support of the function that maps each $b \in \beta$ to the product of $f(a)$ over all $a \in s$ such that $g(a) = b$ is contained in the image of $s$ under $g$.

finprod_mem_finset_product' theorem

 [DecidableEq α] [DecidableEq β] (s : Finset (α × β)) (f : α × β → M) :
  (∏ᶠ (ab) (_ : ab ∈ s), f ab) = ∏ᶠ (a) (b) (_ : b ∈ (s.filter fun ab => Prod.fst ab = a).image Prod.snd), f (a, b)

Full source

/-- Note that `b ∈ (s.filter (fun ab => Prod.fst ab = a)).image Prod.snd` iff `(a, b) ∈ s` so
we can simplify the right hand side of this lemma. However the form stated here is more useful for
iterating this lemma, e.g., if we have `f : α × β × γ → M`. -/
@[to_additive
      "Note that `b ∈ (s.filter (fun ab => Prod.fst ab = a)).image Prod.snd` iff `(a, b) ∈ s` so
      we can simplify the right hand side of this lemma. However the form stated here is more
      useful for iterating this lemma, e.g., if we have `f : α × β × γ → M`."]
theorem finprod_mem_finset_product' [DecidableEq α] [DecidableEq β] (s : Finset (α × β))
    (f : α × β → M) :
    (∏ᶠ (ab) (_ : ab ∈ s), f ab) =
      ∏ᶠ (a) (b) (_ : b ∈ (s.filter fun ab => Prod.fst ab = a).image Prod.snd), f (a, b) := by
  have (a) :
      ∏ i ∈ (s.filter fun ab => Prod.fst ab = a).image Prod.snd, f (a, i) =
        (s.filter (Prod.fst · = a)).prod f := by
    refine Finset.prod_nbij' (fun b ↦ (a, b)) Prod.snd ?_ ?_ ?_ ?_ ?_ <;> aesop
  rw [finprod_mem_finset_eq_prod]
  simp_rw [finprod_mem_finset_eq_prod, this]
  rw [finprod_eq_prod_of_mulSupport_subset _
      (s.mulSupport_of_fiberwise_prod_subset_image f Prod.fst),
    ← Finset.prod_fiberwise_of_maps_to (t := Finset.image Prod.fst s) _ f]
  -- `finish` could close the goal here
  simp only [Finset.mem_image]
  exact fun x hx => ⟨x, hx, rfl⟩

Finite Product over a Finset as Iterated Product: $\prodᶠ_{(a,b) \in s} f(a,b) = \prodᶠ_a \prodᶠ_{b \in s_a} f(a,b)$

Informal description

Let $\alpha$ and $\beta$ be types with decidable equality, $s$ be a finite subset of $\alpha \times \beta$, and $f : \alpha \times \beta \to M$ be a function into a commutative monoid $M$. Then the finite product $\prodᶠ_{(a,b) \in s} f(a,b)$ can be rewritten as $\prodᶠ_{a} \prodᶠ_{b \in \{b' \mid (a,b') \in s\}} f(a,b)$, where for each $a$, the inner product is taken over all $b$ such that $(a,b)$ belongs to $s$.

finprod_mem_finset_product theorem

 (s : Finset (α × β)) (f : α × β → M) : (∏ᶠ (ab) (_ : ab ∈ s), f ab) = ∏ᶠ (a) (b) (_ : (a, b) ∈ s), f (a, b)

Full source

/-- See also `finprod_mem_finset_product'`. -/
@[to_additive "See also `finsum_mem_finset_product'`."]
theorem finprod_mem_finset_product (s : Finset (α × β)) (f : α × β → M) :
    (∏ᶠ (ab) (_ : ab ∈ s), f ab) = ∏ᶠ (a) (b) (_ : (a, b) ∈ s), f (a, b) := by
  classical
    rw [finprod_mem_finset_product']
    simp

Finite product over a finite set as an iterated product: $\prodᶠ_{(a,b) \in s} f(a,b) = \prodᶠ_a \prodᶠ_b f(a,b)$

Informal description

For any finite subset $s$ of $\alpha \times \beta$ and any function $f : \alpha \times \beta \to M$ into a commutative monoid $M$, the finite product $\prodᶠ_{(a,b) \in s} f(a,b)$ is equal to the iterated finite product $\prodᶠ_{a} \prodᶠ_{b} f(a,b)$, where the inner product is taken over all pairs $(a,b)$ in $s$.

finprod_mem_finset_product₃ theorem

 {γ : Type*} (s : Finset (α × β × γ)) (f : α × β × γ → M) :
  (∏ᶠ (abc) (_ : abc ∈ s), f abc) = ∏ᶠ (a) (b) (c) (_ : (a, b, c) ∈ s), f (a, b, c)

Full source

@[to_additive]
theorem finprod_mem_finset_product₃ {γ : Type*} (s : Finset (α × β × γ)) (f : α × β × γ → M) :
    (∏ᶠ (abc) (_ : abc ∈ s), f abc) = ∏ᶠ (a) (b) (c) (_ : (a, b, c) ∈ s), f (a, b, c) := by
  classical
    rw [finprod_mem_finset_product']
    simp_rw [finprod_mem_finset_product']
    simp

Finite product over a triple product set as an iterated product: $\prodᶠ_{(a,b,c) \in s} f(a,b,c) = \prodᶠ_a \prodᶠ_b \prodᶠ_{c \in s_{a,b}} f(a,b,c)$

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types, $s$ be a finite subset of $\alpha \times \beta \times \gamma$, and $f : \alpha \times \beta \times \gamma \to M$ be a function into a commutative monoid $M$. Then the finite product $\prodᶠ_{(a,b,c) \in s} f(a,b,c)$ can be rewritten as $\prodᶠ_{a} \prodᶠ_{b} \prodᶠ_{c \in \{(a,b,c) \in s\}} f(a,b,c)$, where for each pair $(a,b)$, the innermost product is taken over all $c$ such that $(a,b,c)$ belongs to $s$.

finprod_curry theorem

(f : α × β → M) (hf : (mulSupport f).Finite) : ∏ᶠ ab, f ab = ∏ᶠ (a) (b), f (a, b)

Full source

@[to_additive]
theorem finprod_curry (f : α × β → M) (hf : (mulSupport f).Finite) :
    ∏ᶠ ab, f ab = ∏ᶠ (a) (b), f (a, b) := by
  have h₁ : ∀ a, ∏ᶠ _ : a ∈ hf.toFinset, f a = f a := by simp
  have h₂ : ∏ᶠ a, f a = ∏ᶠ (a) (_ : a ∈ hf.toFinset), f a := by simp
  simp_rw [h₂, finprod_mem_finset_product, h₁]

Finite Product Currying: $\prodᶠ_{(a,b)} f(a,b) = \prodᶠ_a \prodᶠ_b f(a,b)$ under Finite Support

Informal description

Let $f \colon \alpha \times \beta \to M$ be a function into a commutative monoid $M$, and suppose the multiplicative support of $f$ (i.e., the set $\{(a,b) \mid f(a,b) \neq 1\}$) is finite. Then the finite product $\prodᶠ_{(a,b)} f(a,b)$ is equal to the iterated finite product $\prodᶠ_{a} \prodᶠ_{b} f(a,b)$.

finprod_curry₃ theorem

 {γ : Type*} (f : α × β × γ → M) (h : (mulSupport f).Finite) : ∏ᶠ abc, f abc = ∏ᶠ (a) (b) (c), f (a, b, c)

Full source

@[to_additive]
theorem finprod_curry₃ {γ : Type*} (f : α × β × γ → M) (h : (mulSupport f).Finite) :
    ∏ᶠ abc, f abc = ∏ᶠ (a) (b) (c), f (a, b, c) := by
  rw [finprod_curry f h]
  congr
  ext a
  rw [finprod_curry]
  simp [h]

Finite Product Currying for Triple Products: $\prodᶠ_{(a,b,c)} f(a,b,c) = \prodᶠ_a \prodᶠ_b \prodᶠ_c f(a,b,c)$ under Finite Support

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types, and let $f \colon \alpha \times \beta \times \gamma \to M$ be a function into a commutative monoid $M$. If the multiplicative support of $f$ (i.e., the set $\{(a,b,c) \mid f(a,b,c) \neq 1\}$) is finite, then the finite product $\prodᶠ_{(a,b,c)} f(a,b,c)$ is equal to the iterated finite product $\prodᶠ_{a} \prodᶠ_{b} \prodᶠ_{c} f(a,b,c)$.

finprod_dmem theorem

 {s : Set α} [DecidablePred (· ∈ s)] (f : ∀ a : α, a ∈ s → M) :
  (∏ᶠ (a : α) (h : a ∈ s), f a h) = ∏ᶠ (a : α) (_ : a ∈ s), if h' : a ∈ s then f a h' else 1

Full source

@[to_additive]
theorem finprod_dmem {s : Set α} [DecidablePred (· ∈ s)] (f : ∀ a : α, a ∈ s → M) :
    (∏ᶠ (a : α) (h : a ∈ s), f a h) = ∏ᶠ (a : α) (_ : a ∈ s), if h' : a ∈ s then f a h' else 1 :=
  finprod_congr fun _ => finprod_congr fun ha => (dif_pos ha).symm

Finite Product over Decidable Membership Set with Conditional Expression

Informal description

Let $s$ be a set in a type $\alpha$ with a decidable membership predicate, and let $f : \Pi (a : \alpha), a \in s \to M$ be a function from elements of $s$ to a commutative monoid $M$. Then the finite product $\prodᶠ_{a \in s} f(a, h)$ (where $h$ is a proof that $a \in s$) is equal to $\prodᶠ_{a \in s} \text{if } a \in s \text{ then } f(a, h') \text{ else } 1$, where $h'$ is another proof that $a \in s$.

finprod_emb_domain' theorem

 {f : α → β} (hf : Injective f) [DecidablePred (· ∈ Set.range f)] (g : α → M) :
  (∏ᶠ b : β, if h : b ∈ Set.range f then g (Classical.choose h) else 1) = ∏ᶠ a : α, g a

Full source

@[to_additive]
theorem finprod_emb_domain' {f : α → β} (hf : Injective f) [DecidablePred (· ∈ Set.range f)]
    (g : α → M) :
    (∏ᶠ b : β, if h : b ∈ Set.range f then g (Classical.choose h) else 1) = ∏ᶠ a : α, g a := by
  simp_rw [← finprod_eq_dif]
  rw [finprod_dmem, finprod_mem_range hf, finprod_congr fun a => _]
  intro a
  rw [dif_pos (Set.mem_range_self a), hf (Classical.choose_spec (Set.mem_range_self a))]

Finite Product Equality for Injective Function's Range

Informal description

Let $f : \alpha \to \beta$ be an injective function between types $\alpha$ and $\beta$, and let $g : \alpha \to M$ be a function from $\alpha$ to a commutative monoid $M$. Suppose the membership in the range of $f$ is decidable. Then the finite product over $\beta$ of the function that maps each $b \in \beta$ to $g(a)$ if $b$ is in the range of $f$ (where $a$ is the unique element such that $f(a) = b$) and to $1$ otherwise, is equal to the finite product of $g$ over $\alpha$. In other words, $$\prodᶠ_{b \in \beta} \begin{cases} g(a) & \text{if } b = f(a) \text{ for some } a \in \alpha \\ 1 & \text{otherwise} \end{cases} = \prodᶠ_{a \in \alpha} g(a).$$

finprod_emb_domain theorem

 (f : α ↪ β) [DecidablePred (· ∈ Set.range f)] (g : α → M) :
  (∏ᶠ b : β, if h : b ∈ Set.range f then g (Classical.choose h) else 1) = ∏ᶠ a : α, g a

Full source

@[to_additive]
theorem finprod_emb_domain (f : α ↪ β) [DecidablePred (· ∈ Set.range f)] (g : α → M) :
    (∏ᶠ b : β, if h : b ∈ Set.range f then g (Classical.choose h) else 1) = ∏ᶠ a : α, g a :=
  finprod_emb_domain' f.injective g

Finite Product Equality for Injective Embedding's Range

Informal description

Let $f \colon \alpha \hookrightarrow \beta$ be an injective function embedding between types $\alpha$ and $\beta$, and let $g \colon \alpha \to M$ be a function from $\alpha$ to a commutative monoid $M$. Suppose membership in the range of $f$ is decidable. Then the finite product over $\beta$ of the function that maps each $b \in \beta$ to $g(a)$ if $b$ is in the range of $f$ (where $a$ is the unique element such that $f(a) = b$) and to $1$ otherwise, is equal to the finite product of $g$ over $\alpha$. In other words, $$ \prod_{b \in \beta} \begin{cases} g(a) & \text{if } b = f(a) \text{ for some } a \in \alpha \\ 1 & \text{otherwise} \end{cases} = \prod_{a \in \alpha} g(a). $$

Mathlib.Algebra.BigOperators.Finprod

Main definitions

Notation

Implementation notes

Tags