doc-next-gen

Mathlib.Algebra.BigOperators.Group.Finset.Defs

Module docstring

{"# Big operators

In this file we define products and sums indexed by finite sets (specifically, Finset).

Notation

We introduce the following notation.

Let s be a Finset α, and f : α → β a function.

  • ∏ x ∈ s, f x is notation for Finset.prod s f (assuming β is a CommMonoid)
  • ∑ x ∈ s, f x is notation for Finset.sum s f (assuming β is an AddCommMonoid)
  • ∏ x, f x is notation for Finset.prod Finset.univ f (assuming α is a Fintype and β is a CommMonoid)
  • ∑ x, f x is notation for Finset.sum Finset.univ f (assuming α is a Fintype and β is an AddCommMonoid)

Implementation Notes

The first arguments in all definitions and lemmas is the codomain of the function of the big operator. This is necessary for the heuristic in @[to_additive]. See the documentation of to_additive.attr for more information.

","### Additive, Multiplicative "}

Finset.prod definition
[CommMonoid β] (s : Finset α) (f : α → β) : β
Full source 
/-- `∏ x ∈ s, f x` is the product of `f x` as `x` ranges over the elements of the finite set `s`.

When the index type is a `Fintype`, the notation `∏ x, f x`, is a shorthand for
`∏ x ∈ Finset.univ, f x`. -/
@[to_additive "`∑ x ∈ s, f x` is the sum of `f x` as `x` ranges over the elements
of the finite set `s`.

When the index type is a `Fintype`, the notation `∑ x, f x`, is a shorthand for
`∑ x ∈ Finset.univ, f x`."]
protected def prod [CommMonoid β] (s : Finset α) (f : α → β) : β :=
  (s.1.map f).prod
Product over a finite set
Informal description
Given a commutative monoid $\beta$, a finite set $s$ of type $\alpha$, and a function $f : \alpha \to \beta$, the product $\prod_{x \in s} f(x)$ is defined as the product of the multiset obtained by applying $f$ to each element of $s$. When the index type $\alpha$ is finite, the notation $\prod_x f(x)$ is shorthand for $\prod_{x \in \text{Finset.univ}} f(x)$.
Finset.prod_mk theorem
[CommMonoid β] (s : Multiset α) (hs : s.Nodup) (f : α → β) : (⟨s, hs⟩ : Finset α).prod f = (s.map f).prod
Full source 
@[to_additive (attr := simp)]
theorem prod_mk [CommMonoid β] (s : Multiset α) (hs : s.Nodup) (f : α → β) :
    (⟨s, hs⟩ : Finset α).prod f = (s.map f).prod :=
  rfl
Product over a Finite Set Constructed from a Nodup Multiset Equals Product of its Image
Informal description
Let $\beta$ be a commutative monoid, $s$ be a multiset over $\alpha$ with no duplicates (i.e., $s.\text{Nodup}$ holds), and $f : \alpha \to \beta$ be a function. Then the product of $f$ over the finite set $\langle s, \text{hs} \rangle$ (constructed from $s$ and its proof of no duplicates) is equal to the product of the multiset obtained by applying $f$ to each element of $s$, i.e., \[ \prod_{x \in \langle s, \text{hs} \rangle} f(x) = \prod_{y \in \text{map } f \ s} y. \]
Finset.prod_val theorem
[CommMonoid α] (s : Finset α) : s.1.prod = s.prod id
Full source 
@[to_additive (attr := simp)]
theorem prod_val [CommMonoid α] (s : Finset α) : s.1.prod = s.prod id := by
  rw [Finset.prod, Multiset.map_id]
Product of Underlying Multiset Equals Product of Identity Function over Finite Set
Informal description
Let $\alpha$ be a commutative monoid and $s$ be a finite subset of $\alpha$. Then the product of the underlying multiset $s.1$ is equal to the product of the identity function over $s$, i.e., \[ \prod_{x \in s.1} x = \prod_{x \in s} \mathrm{id}(x). \]
BigOperators.bigOpBinder definition
: Lean.ParserDescr✝
Full source 
/-- A `bigOpBinder` is like an `extBinder` and has the form `x`, `x : ty`, or `x pred`
where `pred` is a `binderPred` like `< 2`.
Unlike `extBinder`, `x` is a term. -/
syntax bigOpBinder := term:max ((" : " term) <|> binderPred)?
Big operator binder syntax
Informal description
A `bigOpBinder` is a syntax element used in big operators (sums and products) that can take one of three forms: 1. A simple term `x`, 2. A term with a type annotation `x : ty`, or 3. A term with a predicate `x pred` where `pred` is a condition like `< 2`. Unlike `extBinder`, the `x` in a `bigOpBinder` is always treated as a term rather than a pattern.
BigOperators.bigOpBinderParenthesized definition
: Lean.ParserDescr✝
Full source 
/-- A BigOperator binder in parentheses -/
syntax bigOpBinderParenthesized := " (" bigOpBinder ")"
Parenthesized big operator binder
Informal description
A syntax element representing a big operator binder (used in sums and products) enclosed in parentheses. The binder can be: 1. A simple term `x`, 2. A term with a type annotation `x : ty`, or 3. A term with a predicate `x pred` where `pred` is a condition.
BigOperators.bigOpBinderCollection definition
: Lean.ParserDescr✝
Full source 
/-- A list of parenthesized binders -/
syntax bigOpBinderCollection := bigOpBinderParenthesized+
Parenthesized big operator binder collection
Informal description
A syntax element representing a collection of parenthesized binders for big operators (sums and products), where each binder can be: 1. A simple term `x`, 2. A term with a type annotation `x : ty`, or 3. A term with a predicate `x pred` where `pred` is a condition.
BigOperators.bigOpBinders definition
: Lean.ParserDescr✝
Full source 
/-- A single (unparenthesized) binder, or a list of parenthesized binders -/
syntax bigOpBinders := bigOpBinderCollection <|> (ppSpace bigOpBinder)
Big operator binders syntax
Informal description
A syntax element representing either a single unparenthesized binder or a list of parenthesized binders for big operators (sums and products). Each binder can be: 1. A simple term `x`, 2. A term with a type annotation `x : ty`, or 3. A term with a predicate `x pred` where `pred` is a condition like `< 2`.
BigOperators.processBigOpBinder definition
(processed : (Array (Term × Term))) (binder : TSyntax `` bigOpBinder) : MacroM (Array (Term × Term))
Full source 
/-- Collects additional binder/Finset pairs for the given `bigOpBinder`.
Note: this is not extensible at the moment, unlike the usual `bigOpBinder` expansions. -/
def processBigOpBinder (processed : (Array (TermTerm × Term)))
    (binder : TSyntax ``bigOpBinder) : MacroM (Array (TermTerm × Term)) :=
  set_option hygiene false in
  withRef binder do
    match binder with
    | `(bigOpBinder| $x:term) =>
      match x with
      | `(($a + $b = $n)) => -- Maybe this is too cute.
        return processed |>.push (← `(⟨$a, $b⟩), ← `(Finset.Nat.antidiagonal $n))
      | _ => return processed |>.push (x, ← ``(Finset.univ))
    | `(bigOpBinder| $x : $t) => return processed |>.push (x, ← ``((Finset.univ : Finset $t)))
    | `(bigOpBinder| $x ∈ $s) => return processed |>.push (x, ← `(finset% $s))
    | `(bigOpBinder| $x < $n) => return processed |>.push (x, ← `(Finset.Iio $n))
    | `(bigOpBinder| $x ≤ $n) => return processed |>.push (x, ← `(Finset.Iic $n))
    | `(bigOpBinder| $x > $n) => return processed |>.push (x, ← `(Finset.Ioi $n))
    | `(bigOpBinder| $x ≥ $n) => return processed |>.push (x, ← `(Finset.Ici $n))
    | _ => Macro.throwUnsupported
Big operator binder processor
Informal description
The function processes a single binder syntax element for big operators (sums or products), expanding it into pairs of terms and corresponding finite sets. It handles various binder forms including: - Simple terms (interpreted over `Finset.univ`) - Typed terms (interpreted over `Finset.univ` of the specified type) - Membership binders (`x ∈ s` interpreted over the given finset `s`) - Inequality binders (`x < n`, `x ≤ n`, `x > n`, `x ≥ n` interpreted over the corresponding interval finsets) - Special case for `(a + b = n)` interpreted as pairs in the antidiagonal of `n` The processed binders are collected in an array of term-set pairs.
BigOperators.processBigOpBinders definition
(binders : TSyntax `` bigOpBinders) : MacroM (Array (Term × Term))
Full source 
/-- Collects the binder/Finset pairs for the given `bigOpBinders`. -/
def processBigOpBinders (binders : TSyntax ``bigOpBinders) :
    MacroM (Array (TermTerm × Term)) :=
  match binders with
  | `(bigOpBinders| $b:bigOpBinder) => processBigOpBinder #[] b
  | `(bigOpBinders| $[($bs:bigOpBinder)]*) => bs.foldlM processBigOpBinder #[]
  | _ => Macro.throwUnsupported
Big operator binder sequence processor
Informal description
The function processes a sequence of binders for big operators (sums or products), expanding them into an array of term-finset pairs. It handles both single binders and sequences of binders, delegating the processing of individual binders to `processBigOpBinder`. The resulting array contains pairs where each term is associated with its corresponding finite set of values over which the big operator will range.
BigOperators.bigOpBindersPattern definition
(processed : (Array (Term × Term))) : MacroM Term
Full source 
/-- Collect the binderIdents into a `⟨...⟩` expression. -/
def bigOpBindersPattern (processed : (Array (TermTerm × Term))) :
    MacroM Term := do
  let ts := processed.map Prod.fst
  if h : ts.size = 1 then
    return ts[0]
  else
    `(⟨$ts,*⟩)
Pattern construction from term array
Informal description
The function collects an array of term pairs into a single pattern match expression. If the array contains exactly one term, it returns that term directly. Otherwise, it constructs a tuple pattern `⟨...⟩` containing all the terms from the array.
BigOperators.bigOpBindersProd definition
(processed : (Array (Term × Term))) : MacroM Term
Full source 
/-- Collect the terms into a product of sets. -/
def bigOpBindersProd (processed : (Array (TermTerm × Term))) :
    MacroM Term := do
  if h₀ : processed.size = 0 then
    `((Finset.univ : Finset Unit))
  else if h₁ : processed.size = 1 then
    return processed[0].2
  else
    processed.foldrM (fun s p => `(SProd.sprod $(s.2) $p)) processed.back.2
      (start := processed.size - 1)
Product of sets for big operators
Informal description
Given an array of pairs of terms, this function constructs the product of sets for big operators. If the array is empty, it returns the universal finset of the unit type. If the array has exactly one element, it returns the second component of that element. Otherwise, it constructs the product of sets by folding the array from right to left using the `SProd.sprod` operation.
BigOperators.bigsum definition
: Lean.ParserDescr✝
Full source 
/--
- `∑ x, f x` is notation for `Finset.sum Finset.univ f`. It is the sum of `f x`,
  where `x` ranges over the finite domain of `f`.
- `∑ x ∈ s, f x` is notation for `Finset.sum s f`. It is the sum of `f x`,
  where `x` ranges over the finite set `s` (either a `Finset` or a `Set` with a `Fintype` instance).
- `∑ x ∈ s with p x, f x` is notation for `Finset.sum (Finset.filter p s) f`.
- `∑ (x ∈ s) (y ∈ t), f x y` is notation for `Finset.sum (s ×ˢ t) (fun ⟨x, y⟩ ↦ f x y)`.

These support destructuring, for example `∑ ⟨x, y⟩ ∈ s ×ˢ t, f x y`.

Notation: `"∑" bigOpBinders* ("with" term)? "," term` -/
syntax (name := bigsum) "∑ " bigOpBinders ("with " term)? ", " term:67 : term
Summation notation over finite sets
Informal description
The notation $\sum x, f x$ represents the sum of $f x$ over all $x$ in the finite domain of $f$, equivalent to `Finset.sum Finset.univ f`. More generally: - $\sum x \in s, f x$ denotes the sum of $f x$ over all $x$ in the finite set $s$ (either a `Finset` or a `Set` with a `Fintype` instance). - $\sum x \in s \text{ with } p x, f x$ denotes the sum of $f x$ over all $x$ in $s$ satisfying the predicate $p$. - $\sum (x \in s) (y \in t), f x y$ denotes the sum of $f x y$ over all pairs $(x, y)$ in the Cartesian product $s \times t$. This notation supports destructuring, e.g., $\sum \langle x, y \rangle \in s \times t, f x y$.
BigOperators.bigprod definition
: Lean.ParserDescr✝
Full source 
/--
- `∏ x, f x` is notation for `Finset.prod Finset.univ f`. It is the product of `f x`,
  where `x` ranges over the finite domain of `f`.
- `∏ x ∈ s, f x` is notation for `Finset.prod s f`. It is the product of `f x`,
  where `x` ranges over the finite set `s` (either a `Finset` or a `Set` with a `Fintype` instance).
- `∏ x ∈ s with p x, f x` is notation for `Finset.prod (Finset.filter p s) f`.
- `∏ (x ∈ s) (y ∈ t), f x y` is notation for `Finset.prod (s ×ˢ t) (fun ⟨x, y⟩ ↦ f x y)`.

These support destructuring, for example `∏ ⟨x, y⟩ ∈ s ×ˢ t, f x y`.

Notation: `"∏" bigOpBinders* ("with" term)? "," term` -/
syntax (name := bigprod) "∏ " bigOpBinders ("with " term)? ", " term:67 : term
Product notation over finite sets
Informal description
The notation $\prod x, f x$ represents the product of $f x$ over all $x$ in the finite domain of $f$, equivalent to `Finset.prod Finset.univ f`. More generally: - $\prod x \in s, f x$ denotes the product of $f x$ over all $x$ in the finite set $s$ (either a `Finset` or a `Set` with a `Fintype` instance). - $\prod x \in s \text{ with } p x, f x$ denotes the product of $f x$ over all $x$ in $s$ satisfying the predicate $p$. - $\prod (x \in s) (y \in t), f x y$ denotes the product of $f x y$ over all pairs $(x, y)$ in the Cartesian product $s \times t$. This notation supports destructuring, e.g., $\prod \langle x, y \rangle \in s \times t, f x y$.
BigOperators.bigsumin definition
: Lean.ParserDescr✝
Full source 
/-- Deprecated, use `∑ x ∈ s, f x` instead. -/
syntax (name := bigsumin) "∑ " extBinder " in " term ", " term:67 : term
Sum over finite set (deprecated notation)
Informal description
The notation `∑ x in s, f x` represents the sum of the function `f` over all elements `x` in the finite set `s`. This is equivalent to `Finset.sum s f` when the codomain is an additive commutative monoid. **Note:** This notation is deprecated and the preferred notation is `∑ x ∈ s, f x`.
BigOperators.bigprodin definition
: Lean.ParserDescr✝
Full source 
/-- Deprecated, use `∏ x ∈ s, f x` instead. -/
syntax (name := bigprodin) "∏ " extBinder " in " term ", " term:67 : term
Deprecated product notation over a finite set
Informal description
The notation `∏ x ∈ s, f x` represents the product of the function `f` evaluated at each element `x` in the finite set `s`. This is the deprecated version of the notation, and it is recommended to use the newer notation `∏ x ∈ s, f x` instead.
BigOperators.delabFinsetProd definition
: Delab
Full source 
/-- Delaborator for `Finset.prod`. The `pp.funBinderTypes` option controls whether
to show the domain type when the product is over `Finset.univ`. -/
@[app_delab Finset.prod] def delabFinsetProd : Delab :=
  whenPPOption getPPNotation <| withOverApp 5 <| do
  let #[_, _, _, s, f] := (← getExpr).getAppArgs | failure
  guardguard <| f.isLambda
  let ppDomain ← getPPOption getPPFunBinderTypes
  let (i, body) ← withAppArg <| withBindingBodyUnusedName fun i => do
    return (i, ← delab)
  if s.isAppOfArity ``Finset.univ 2 then
    let binder ←
      if ppDomain then
        let ty ← withNaryArg 0 delab
        `(bigOpBinder| $(.mk i):ident : $ty)
      else
        `(bigOpBinder| $(.mk i):ident)
    `(∏ $binder:bigOpBinder, $body)
  else
    let ss ← withNaryArg 3 <| delab
    `(∏ $(.mk i):ident ∈ $ss, $body)
Product notation delaborator
Informal description
The delaborator for the notation `∏ x ∈ s, f x` representing the product of `f x` over all `x` in the finite set `s`. When the product is taken over `Finset.univ` (the universal finite set of a type), the notation simplifies to `∏ x, f x`. The display of the domain type in the binder is controlled by the pretty-printing option `pp.funBinderTypes`.
BigOperators.delabFinsetSum definition
: Delab
Full source 
/-- Delaborator for `Finset.sum`. The `pp.funBinderTypes` option controls whether
to show the domain type when the sum is over `Finset.univ`. -/
@[app_delab Finset.sum] def delabFinsetSum : Delab :=
  whenPPOption getPPNotation <| withOverApp 5 <| do
  let #[_, _, _, s, f] := (← getExpr).getAppArgs | failure
  guardguard <| f.isLambda
  let ppDomain ← getPPOption getPPFunBinderTypes
  let (i, body) ← withAppArg <| withBindingBodyUnusedName fun i => do
    return (i, ← delab)
  if s.isAppOfArity ``Finset.univ 2 then
    let binder ←
      if ppDomain then
        let ty ← withNaryArg 0 delab
        `(bigOpBinder| $(.mk i):ident : $ty)
      else
        `(bigOpBinder| $(.mk i):ident)
    `(∑ $binder:bigOpBinder, $body)
  else
    let ss ← withNaryArg 3 <| delab
    `(∑ $(.mk i):ident ∈ $ss, $body)
Delaborator for Finset Sum Notation
Informal description
The delaborator for `Finset.sum` notation, which controls how the summation expression is pretty-printed. When the sum is over `Finset.univ`, the domain type is optionally shown based on the `pp.funBinderTypes` setting. The delaborator handles both forms: `∑ x ∈ s, f x` for a specific finset `s` and `∑ x, f x` for sums over the entire universe of a finite type.
Finset.prod_eq_multiset_prod theorem
[CommMonoid β] (s : Finset α) (f : α → β) : ∏ x ∈ s, f x = (s.1.map f).prod
Full source 
@[to_additive]
theorem prod_eq_multiset_prod [CommMonoid β] (s : Finset α) (f : α → β) :
    ∏ x ∈ s, f x = (s.1.map f).prod :=
  rfl
Equality of Finset Product and Multiset Image Product
Informal description
Let $\beta$ be a commutative monoid, $s$ a finite set of type $\alpha$, and $f : \alpha \to \beta$ a function. The product of $f$ over $s$ equals the product of the multiset obtained by applying $f$ to each element of the underlying multiset of $s$, i.e., $$\prod_{x \in s} f(x) = \prod_{y \in \text{map } f \ s.1} y.$$
Finset.prod_map_val theorem
[CommMonoid β] (s : Finset α) (f : α → β) : (s.1.map f).prod = ∏ a ∈ s, f a
Full source 
@[to_additive (attr := simp)]
lemma prod_map_val [CommMonoid β] (s : Finset α) (f : α → β) : (s.1.map f).prod = ∏ a ∈ s, f a :=
  rfl
Equality of Multiset Image Product and Finset Product
Informal description
Let $\beta$ be a commutative monoid, $s$ a finite set of type $\alpha$, and $f : \alpha \to \beta$ a function. The product of the multiset obtained by applying $f$ to each element of the underlying multiset of $s$ is equal to the product of $f$ over $s$, i.e., $$ \prod_{a \in \text{map } f \ s.1} a = \prod_{a \in s} f(a). $$
Finset.sum_multiset_singleton theorem
(s : Finset α) : ∑ a ∈ s, { a } = s.val
Full source 
@[simp]
theorem sum_multiset_singleton (s : Finset α) : ∑ a ∈ s, {a} = s.val := by
  simp only [sum_eq_multiset_sum, Multiset.sum_map_singleton]
Sum of Singletons Equals Underlying Multiset
Informal description
For any finite set $s$ of type $\alpha$, the sum of singleton multisets $\{a\}$ over all elements $a \in s$ equals the underlying multiset $s.val$ of $s$.
map_prod theorem
[CommMonoid β] [CommMonoid γ] {G : Type*} [FunLike G β γ] [MonoidHomClass G β γ] (g : G) (f : α → β) (s : Finset α) : g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x)
Full source 
@[to_additive (attr := simp)]
theorem map_prod [CommMonoid β] [CommMonoid γ] {G : Type*} [FunLike G β γ] [MonoidHomClass G β γ]
    (g : G) (f : α → β) (s : Finset α) : g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x) := by
  simp only [Finset.prod_eq_multiset_prod, map_multiset_prod, Multiset.map_map]; rfl
Homomorphism Commutes with Finite Product: $g\left( \prod_{x \in s} f(x) \right) = \prod_{x \in s} g(f(x))$
Informal description
Let $\beta$ and $\gamma$ be commutative monoids, and let $G$ be a type of homomorphisms from $\beta$ to $\gamma$ that preserve the monoid structure. For any homomorphism $g \in G$, any function $f : \alpha \to \beta$, and any finite set $s$ of type $\alpha$, we have \[ g\left( \prod_{x \in s} f(x) \right) = \prod_{x \in s} g(f(x)). \]
Finset.prod_empty theorem
: ∏ x ∈ ∅, f x = 1
Full source 
@[to_additive (attr := simp)]
theorem prod_empty : ∏ x ∈ ∅, f x = 1 :=
  rfl
Empty Product Equals One: $\prod_{x \in \emptyset} f(x) = 1$
Informal description
The product of a function $f$ over the empty set is equal to the multiplicative identity $1$, i.e., \[ \prod_{x \in \emptyset} f(x) = 1. \]
Finset.prod_of_isEmpty theorem
[IsEmpty α] (s : Finset α) : ∏ i ∈ s, f i = 1
Full source 
@[to_additive]
theorem prod_of_isEmpty [IsEmpty α] (s : Finset α) : ∏ i ∈ s, f i = 1 := by
  rw [eq_empty_of_isEmpty s, prod_empty]
Product over Empty Type Equals One: $\prod_{i \in s} f(i) = 1$ when $\alpha$ is empty
Informal description
For any type $\alpha$ that is empty (has no elements) and any finite subset $s$ of $\alpha$, the product $\prod_{i \in s} f(i)$ equals the multiplicative identity $1$.
Finset.prod_const_one theorem
: (∏ _x ∈ s, (1 : β)) = 1
Full source 
@[to_additive (attr := simp)]
theorem prod_const_one : (∏ _x ∈ s, (1 : β)) = 1 := by
  simp only [Finset.prod, Multiset.map_const', Multiset.prod_replicate, one_pow]
Product of Constant One Function over Finite Set Equals One
Informal description
For any finite set $s$ and any commutative monoid $\beta$, the product of the constant function $1$ over $s$ equals the multiplicative identity $1$, i.e., \[ \prod_{x \in s} 1 = 1. \]
Finset.prod_map theorem
(s : Finset α) (e : α ↪ γ) (f : γ → β) : ∏ x ∈ s.map e, f x = ∏ x ∈ s, f (e x)
Full source 
@[to_additive (attr := simp)]
theorem prod_map (s : Finset α) (e : α ↪ γ) (f : γ → β) :
    ∏ x ∈ s.map e, f x = ∏ x ∈ s, f (e x) := by
  rw [Finset.prod, Finset.map_val, Multiset.map_map]; rfl
Product over Image of Finite Set under Injective Embedding
Informal description
Let $s$ be a finite subset of a type $\alpha$, $e : \alpha \hookrightarrow \gamma$ an injective function embedding, and $f : \gamma \to \beta$ a function where $\beta$ is a commutative monoid. Then the product of $f$ over the image of $s$ under $e$ equals the product of $f \circ e$ over $s$: \[ \prod_{x \in e(s)} f(x) = \prod_{x \in s} f(e(x)). \]
Finset.prod_map_toList theorem
(s : Finset α) (f : α → β) : (s.toList.map f).prod = s.prod f
Full source 
@[to_additive (attr := simp)]
theorem prod_map_toList (s : Finset α) (f : α → β) : (s.toList.map f).prod = s.prod f := by
  rw [Finset.prod, ← Multiset.prod_coe, ← Multiset.map_coe, Finset.coe_toList]
Equality of List-Mapped Product and Finset Product
Informal description
For any finite set $s$ of type $\alpha$ and any function $f : \alpha \to \beta$ where $\beta$ is a commutative monoid, the product of the list obtained by applying $f$ to each element of $s$ (via `toList.map`) equals the product of $f$ over $s$. That is, $\prod (s.\text{toList}.\text{map}\, f) = \prod_{x \in s} f(x)$.
Finset.prod_toList theorem
{α : Type*} [CommMonoid α] (s : Finset α) : s.toList.prod = ∏ x ∈ s, x
Full source 
@[to_additive (attr := simp)]
theorem prod_toList {α : Type*} [CommMonoid α] (s : Finset α) :
    s.toList.prod = ∏ x ∈ s, x := by
  simpa using s.prod_map_toList id
Equality of List Product and Finset Product in a Commutative Monoid
Informal description
For any finite set $s$ of elements in a commutative monoid $\alpha$, the product of the elements in the list representation of $s$ equals the product of the elements in $s$. That is, $\prod (s.\text{toList}) = \prod_{x \in s} x$.
Equiv.Perm.prod_comp theorem
(σ : Equiv.Perm α) (s : Finset α) (f : α → β) (hs : {a | σ a ≠ a} ⊆ s) : (∏ x ∈ s, f (σ x)) = ∏ x ∈ s, f x
Full source 
@[to_additive]
theorem _root_.Equiv.Perm.prod_comp (σ : Equiv.Perm α) (s : Finset α) (f : α → β)
    (hs : { a | σ a ≠ a }{ a | σ a ≠ a } ⊆ s) : (∏ x ∈ s, f (σ x)) = ∏ x ∈ s, f x := by
  convert (prod_map s σ.toEmbedding f).symm
  exact (map_perm hs).symm
Invariance of Finite Product under Permutation: $\prod_{x \in s} f(\sigma(x)) = \prod_{x \in s} f(x)$ when $\sigma$ moves only elements in $s$
Informal description
Let $\sigma$ be a permutation of a type $\alpha$, $s$ a finite subset of $\alpha$, and $f : \alpha \to \beta$ a function where $\beta$ is a commutative monoid. If the set of elements not fixed by $\sigma$ is contained in $s$ (i.e., $\{a \in \alpha \mid \sigma(a) \neq a\} \subseteq s$), then the product of $f$ over the image of $s$ under $\sigma$ equals the product of $f$ over $s$: \[ \prod_{x \in s} f(\sigma(x)) = \prod_{x \in s} f(x). \]
Equiv.Perm.prod_comp' theorem
(σ : Equiv.Perm α) (s : Finset α) (f : α → α → β) (hs : {a | σ a ≠ a} ⊆ s) : (∏ x ∈ s, f (σ x) x) = ∏ x ∈ s, f x (σ.symm x)
Full source 
@[to_additive]
theorem _root_.Equiv.Perm.prod_comp' (σ : Equiv.Perm α) (s : Finset α) (f : α → α → β)
    (hs : { a | σ a ≠ a }{ a | σ a ≠ a } ⊆ s) : (∏ x ∈ s, f (σ x) x) = ∏ x ∈ s, f x (σ.symm x) := by
  convert σ.prod_comp s (fun x => f x (σ.symm x)) hs
  rw [Equiv.symm_apply_apply]
Product Invariance under Permutation with Two Arguments: $\prod_{x \in s} f(\sigma(x), x) = \prod_{x \in s} f(x, \sigma^{-1}(x))$ when $\sigma$ moves only elements in $s$
Informal description
Let $\sigma$ be a permutation of a type $\alpha$, $s$ a finite subset of $\alpha$, and $f : \alpha \times \alpha \to \beta$ a function where $\beta$ is a commutative monoid. If the set of elements not fixed by $\sigma$ is contained in $s$ (i.e., $\{a \in \alpha \mid \sigma(a) \neq a\} \subseteq s$), then the following product equality holds: \[ \prod_{x \in s} f(\sigma(x), x) = \prod_{x \in s} f(x, \sigma^{-1}(x)). \]
Finset.prod_bij theorem
(i : ∀ a ∈ s, κ) (hi : ∀ a ha, i a ha ∈ t) (i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) (i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) (h : ∀ a ha, f a = g (i a ha)) : ∏ x ∈ s, f x = ∏ x ∈ t, g x
Full source 
/-- Reorder a product.

The difference with `Finset.prod_bij'` is that the bijection is specified as a surjective injection,
rather than by an inverse function.

The difference with `Finset.prod_nbij` is that the bijection is allowed to use membership of the
domain of the product, rather than being a non-dependent function. -/
@[to_additive "Reorder a sum.

The difference with `Finset.sum_bij'` is that the bijection is specified as a surjective injection,
rather than by an inverse function.

The difference with `Finset.sum_nbij` is that the bijection is allowed to use membership of the
domain of the sum, rather than being a non-dependent function."]
theorem prod_bij (i : ∀ a ∈ s, κ) (hi : ∀ a ha, i a ha ∈ t)
    (i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
    (i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) (h : ∀ a ha, f a = g (i a ha)) :
    ∏ x ∈ s, f x = ∏ x ∈ t, g x :=
  congr_arg Multiset.prod (Multiset.map_eq_map_of_bij_of_nodup f g s.2 t.2 i hi i_inj i_surj h)
Product Equality under Bijective Correspondence
Informal description
Let $s$ and $t$ be finite sets, and let $f : \alpha \to \beta$ and $g : \kappa \to \beta$ be functions where $\beta$ is a commutative monoid. Suppose there exists a function $i : \alpha \to \kappa$ defined for all $a \in s$ such that: 1. For every $a \in s$, $i(a) \in t$, 2. $i$ is injective on $s$: for any $a_1, a_2 \in s$, if $i(a_1) = i(a_2)$ then $a_1 = a_2$, 3. $i$ is surjective onto $t$: for every $b \in t$, there exists $a \in s$ such that $i(a) = b$, 4. The functions agree on corresponding elements: $f(a) = g(i(a))$ for all $a \in s$. Then the products satisfy $\prod_{x \in s} f(x) = \prod_{x \in t} g(x)$.
Finset.prod_bij' theorem
(i : ∀ a ∈ s, κ) (j : ∀ a ∈ t, ι) (hi : ∀ a ha, i a ha ∈ t) (hj : ∀ a ha, j a ha ∈ s) (left_inv : ∀ a ha, j (i a ha) (hi a ha) = a) (right_inv : ∀ a ha, i (j a ha) (hj a ha) = a) (h : ∀ a ha, f a = g (i a ha)) : ∏ x ∈ s, f x = ∏ x ∈ t, g x
Full source 
/-- Reorder a product.

The difference with `Finset.prod_bij` is that the bijection is specified with an inverse, rather
than as a surjective injection.

The difference with `Finset.prod_nbij'` is that the bijection and its inverse are allowed to use
membership of the domains of the products, rather than being non-dependent functions. -/
@[to_additive "Reorder a sum.

The difference with `Finset.sum_bij` is that the bijection is specified with an inverse, rather than
as a surjective injection.

The difference with `Finset.sum_nbij'` is that the bijection and its inverse are allowed to use
membership of the domains of the sums, rather than being non-dependent functions."]
theorem prod_bij' (i : ∀ a ∈ s, κ) (j : ∀ a ∈ t, ι) (hi : ∀ a ha, i a ha ∈ t)
    (hj : ∀ a ha, j a ha ∈ s) (left_inv : ∀ a ha, j (i a ha) (hi a ha) = a)
    (right_inv : ∀ a ha, i (j a ha) (hj a ha) = a) (h : ∀ a ha, f a = g (i a ha)) :
    ∏ x ∈ s, f x = ∏ x ∈ t, g x := by
  refine prod_bij i hi (fun a1 h1 a2 h2 eq ↦ ?_) (fun b hb ↦ ⟨_, hj b hb, right_inv b hb⟩) h
  rw [← left_inv a1 h1, ← left_inv a2 h2]
  simp only [eq]
Product Equality under Bijective Correspondence with Explicit Inverse
Informal description
Let $s$ and $t$ be finite sets, and let $f : \alpha \to \beta$ and $g : \kappa \to \beta$ be functions where $\beta$ is a commutative monoid. Suppose there exist functions $i : \alpha \to \kappa$ and $j : \kappa \to \alpha$ defined for all $a \in s$ and $b \in t$ respectively, such that: 1. For every $a \in s$, $i(a) \in t$, 2. For every $b \in t$, $j(b) \in s$, 3. $j$ is a left inverse of $i$: $j(i(a)) = a$ for all $a \in s$, 4. $i$ is a right inverse of $j$: $i(j(b)) = b$ for all $b \in t$, 5. The functions agree on corresponding elements: $f(a) = g(i(a))$ for all $a \in s$. Then the products satisfy $\prod_{x \in s} f(x) = \prod_{x \in t} g(x)$.
Finset.prod_nbij theorem
(i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (i_inj : (s : Set ι).InjOn i) (i_surj : (s : Set ι).SurjOn i t) (h : ∀ a ∈ s, f a = g (i a)) : ∏ x ∈ s, f x = ∏ x ∈ t, g x
Full source 
/-- Reorder a product.

The difference with `Finset.prod_nbij'` is that the bijection is specified as a surjective
injection, rather than by an inverse function.

The difference with `Finset.prod_bij` is that the bijection is a non-dependent function, rather than
being allowed to use membership of the domain of the product. -/
@[to_additive "Reorder a sum.

The difference with `Finset.sum_nbij'` is that the bijection is specified as a surjective injection,
rather than by an inverse function.

The difference with `Finset.sum_bij` is that the bijection is a non-dependent function, rather than
being allowed to use membership of the domain of the sum."]
lemma prod_nbij (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (i_inj : (s : Set ι).InjOn i)
    (i_surj : (s : Set ι).SurjOn i t) (h : ∀ a ∈ s, f a = g (i a)) :
    ∏ x ∈ s, f x = ∏ x ∈ t, g x :=
  prod_bij (fun a _ ↦ i a) hi i_inj (by simpa using i_surj) h
Product Equality under Non-Dependent Bijective Correspondence
Informal description
Let $s$ be a finite subset of $\iota$ and $t$ a finite subset of $\kappa$, and let $f : \iota \to \beta$ and $g : \kappa \to \beta$ be functions where $\beta$ is a commutative monoid. Suppose there exists a function $i : \iota \to \kappa$ such that: 1. For every $a \in s$, $i(a) \in t$, 2. $i$ is injective on $s$: for any $x_1, x_2 \in s$, if $i(x_1) = i(x_2)$ then $x_1 = x_2$, 3. $i$ is surjective onto $t$: for every $b \in t$, there exists $a \in s$ such that $i(a) = b$, 4. The functions agree on corresponding elements: $f(a) = g(i(a))$ for all $a \in s$. Then the products satisfy $\prod_{x \in s} f(x) = \prod_{x \in t} g(x)$.
Finset.prod_nbij' theorem
(i : ι → κ) (j : κ → ι) (hi : ∀ a ∈ s, i a ∈ t) (hj : ∀ a ∈ t, j a ∈ s) (left_inv : ∀ a ∈ s, j (i a) = a) (right_inv : ∀ a ∈ t, i (j a) = a) (h : ∀ a ∈ s, f a = g (i a)) : ∏ x ∈ s, f x = ∏ x ∈ t, g x
Full source 
/-- Reorder a product.

The difference with `Finset.prod_nbij` is that the bijection is specified with an inverse, rather
than as a surjective injection.

The difference with `Finset.prod_bij'` is that the bijection and its inverse are non-dependent
functions, rather than being allowed to use membership of the domains of the products.

The difference with `Finset.prod_equiv` is that bijectivity is only required to hold on the domains
of the products, rather than on the entire types.
-/
@[to_additive "Reorder a sum.

The difference with `Finset.sum_nbij` is that the bijection is specified with an inverse, rather
than as a surjective injection.

The difference with `Finset.sum_bij'` is that the bijection and its inverse are non-dependent
functions, rather than being allowed to use membership of the domains of the sums.

The difference with `Finset.sum_equiv` is that bijectivity is only required to hold on the domains
of the sums, rather than on the entire types."]
lemma prod_nbij' (i : ι → κ) (j : κ → ι) (hi : ∀ a ∈ s, i a ∈ t) (hj : ∀ a ∈ t, j a ∈ s)
    (left_inv : ∀ a ∈ s, j (i a) = a) (right_inv : ∀ a ∈ t, i (j a) = a)
    (h : ∀ a ∈ s, f a = g (i a)) : ∏ x ∈ s, f x = ∏ x ∈ t, g x :=
  prod_bij' (fun a _ ↦ i a) (fun b _ ↦ j b) hi hj left_inv right_inv h
Product Equality under Non-Dependent Bijective Correspondence with Explicit Inverse
Informal description
Let $s$ be a finite subset of $\iota$ and $t$ a finite subset of $\kappa$, and let $f : \iota \to \beta$ and $g : \kappa \to \beta$ be functions where $\beta$ is a commutative monoid. Suppose there exist functions $i : \iota \to \kappa$ and $j : \kappa \to \iota$ such that: 1. For every $a \in s$, $i(a) \in t$, 2. For every $b \in t$, $j(b) \in s$, 3. $j$ is a left inverse of $i$ on $s$: $j(i(a)) = a$ for all $a \in s$, 4. $i$ is a right inverse of $j$ on $t$: $i(j(b)) = b$ for all $b \in t$, 5. The functions agree on corresponding elements: $f(a) = g(i(a))$ for all $a \in s$. Then the products satisfy $\prod_{x \in s} f(x) = \prod_{x \in t} g(x)$.
Finset.prod_equiv theorem
(e : ι ≃ κ) (hst : ∀ i, i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) : ∏ i ∈ s, f i = ∏ i ∈ t, g i
Full source 
/-- Specialization of `Finset.prod_nbij'` that automatically fills in most arguments.

See `Fintype.prod_equiv` for the version where `s` and `t` are `univ`. -/
@[to_additive "`Specialization of `Finset.sum_nbij'` that automatically fills in most arguments.

See `Fintype.sum_equiv` for the version where `s` and `t` are `univ`."]
lemma prod_equiv (e : ι ≃ κ) (hst : ∀ i, i ∈ si ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) :
    ∏ i ∈ s, f i = ∏ i ∈ t, g i := by refine prod_nbij' e e.symm ?_ ?_ ?_ ?_ hfg <;> simp [hst]
Product Equality under Bijective Equivalence: $\prod_{i \in s} f(i) = \prod_{i \in t} g(i)$
Informal description
Let $s$ be a finite subset of $\iota$ and $t$ a finite subset of $\kappa$, and let $f : \iota \to \beta$ and $g : \kappa \to \beta$ be functions where $\beta$ is a commutative monoid. Given a bijection $e : \iota \simeq \kappa$ such that: 1. For every $i \in \iota$, $i \in s$ if and only if $e(i) \in t$, 2. For every $i \in s$, $f(i) = g(e(i))$, then the products satisfy $\prod_{i \in s} f(i) = \prod_{i \in t} g(i)$.
Finset.prod_bijective theorem
(e : ι → κ) (he : e.Bijective) (hst : ∀ i, i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) : ∏ i ∈ s, f i = ∏ i ∈ t, g i
Full source 
/-- Specialization of `Finset.prod_bij` that automatically fills in most arguments.

See `Fintype.prod_bijective` for the version where `s` and `t` are `univ`. -/
@[to_additive "`Specialization of `Finset.sum_bij` that automatically fills in most arguments.

See `Fintype.sum_bijective` for the version where `s` and `t` are `univ`."]
lemma prod_bijective (e : ι → κ) (he : e.Bijective) (hst : ∀ i, i ∈ si ∈ s ↔ e i ∈ t)
    (hfg : ∀ i ∈ s, f i = g (e i)) :
    ∏ i ∈ s, f i = ∏ i ∈ t, g i := prod_equiv (.ofBijective e he) hst hfg
Product Equality under Bijective Index Transformation: $\prod_{i \in s} f(i) = \prod_{i \in t} g(i)$
Informal description
Let $s$ be a finite subset of $\iota$ and $t$ a finite subset of $\kappa$, and let $f : \iota \to \beta$ and $g : \kappa \to \beta$ be functions where $\beta$ is a commutative monoid. Given a bijective function $e : \iota \to \kappa$ such that: 1. For every $i \in \iota$, $i \in s$ if and only if $e(i) \in t$, 2. For every $i \in s$, $f(i) = g(e(i))$, then the products satisfy $\prod_{i \in s} f(i) = \prod_{i \in t} g(i)$.
Finset.prod_hom_rel theorem
[CommMonoid γ] {r : β → γ → Prop} {f : α → β} {g : α → γ} {s : Finset α} (h₁ : r 1 1) (h₂ : ∀ a b c, r b c → r (f a * b) (g a * c)) : r (∏ x ∈ s, f x) (∏ x ∈ s, g x)
Full source 
@[to_additive]
theorem prod_hom_rel [CommMonoid γ] {r : β → γ → Prop} {f : α → β} {g : α → γ} {s : Finset α}
    (h₁ : r 1 1) (h₂ : ∀ a b c, r b c → r (f a * b) (g a * c)) :
    r (∏ x ∈ s, f x) (∏ x ∈ s, g x) := by
  delta Finset.prod
  apply Multiset.prod_hom_rel <;> assumption
Product Homomorphism-Relation Compatibility
Informal description
Let $\beta$ and $\gamma$ be commutative monoids, and let $r : \beta \to \gamma \to \text{Prop}$ be a relation. Given functions $f : \alpha \to \beta$ and $g : \alpha \to \gamma$, and a finite set $s \subseteq \alpha$, suppose that: 1. $r$ relates the identity elements: $r(1_\beta, 1_\gamma)$. 2. For all $a \in \alpha$ and $b \in \beta, c \in \gamma$, if $r(b, c)$ holds, then $r(f(a) \cdot b, g(a) \cdot c)$ also holds. Then, $r$ relates the products over $s$: \[ r\left(\prod_{x \in s} f(x), \prod_{x \in s} g(x)\right). \]
Finset.prod_coe_sort_eq_attach theorem
(f : s → β) : ∏ i : s, f i = ∏ i ∈ s.attach, f i
Full source 
@[to_additive]
theorem prod_coe_sort_eq_attach (f : s → β) : ∏ i : s, f i = ∏ i ∈ s.attach, f i :=
  rfl
Product over Subtype Equals Product over Attached Finset
Informal description
For any finite set $s$ of elements of type $\alpha$ and any function $f : \{x \mid x \in s\} \to \beta$ into a commutative monoid $\beta$, the product of $f$ over the subtype $\{x \mid x \in s\}$ is equal to the product of $f$ over the attached finite set $s.\text{attach}$. In symbols: \[ \prod_{i \in \{x \mid x \in s\}} f(i) = \prod_{i \in s.\text{attach}} f(i). \]
Finset.prod_ite_index theorem
(p : Prop) [Decidable p] (s t : Finset α) (f : α → β) : ∏ x ∈ if p then s else t, f x = if p then ∏ x ∈ s, f x else ∏ x ∈ t, f x
Full source 
@[to_additive]
theorem prod_ite_index (p : Prop) [Decidable p] (s t : Finset α) (f : α → β) :
    ∏ x ∈ if p then s else t, f x = if p then ∏ x ∈ s, f x else ∏ x ∈ t, f x :=
  apply_ite (fun s => ∏ x ∈ s, f x) _ _ _
Conditional Product over Finite Sets
Informal description
Let $p$ be a decidable proposition, $s$ and $t$ be finite sets of elements of type $\alpha$, and $f : \alpha \to \beta$ be a function into a commutative monoid $\beta$. Then the product of $f$ over the set $\text{if } p \text{ then } s \text{ else } t$ is equal to $\prod_{x \in s} f(x)$ if $p$ holds, and $\prod_{x \in t} f(x)$ otherwise. In symbols: \[ \prod_{x \in (\text{if } p \text{ then } s \text{ else } t)} f(x) = \text{if } p \text{ then } \prod_{x \in s} f(x) \text{ else } \prod_{x \in t} f(x). \]
Finset.prod_ite_irrel theorem
(p : Prop) [Decidable p] (s : Finset α) (f g : α → β) : ∏ x ∈ s, (if p then f x else g x) = if p then ∏ x ∈ s, f x else ∏ x ∈ s, g x
Full source 
@[to_additive (attr := simp)]
theorem prod_ite_irrel (p : Prop) [Decidable p] (s : Finset α) (f g : α → β) :
    ∏ x ∈ s, (if p then f x else g x) = if p then ∏ x ∈ s, f x else ∏ x ∈ s, g x := by
  split_ifs with h <;> rfl
Conditional Product Equality for Finite Sets
Informal description
Let $p$ be a decidable proposition, $s$ be a finite set of elements of type $\alpha$, and $f, g : \alpha \to \beta$ be functions into a commutative monoid $\beta$. Then the product over $s$ of the function that evaluates to $f(x)$ if $p$ holds and $g(x)$ otherwise is equal to the product of $f$ over $s$ if $p$ holds, and the product of $g$ over $s$ otherwise. In symbols: \[ \prod_{x \in s} \left(\text{if } p \text{ then } f(x) \text{ else } g(x)\right) = \text{if } p \text{ then } \prod_{x \in s} f(x) \text{ else } \prod_{x \in s} g(x). \]
Finset.prod_dite_irrel theorem
(p : Prop) [Decidable p] (s : Finset α) (f : p → α → β) (g : ¬p → α → β) : ∏ x ∈ s, (if h : p then f h x else g h x) = if h : p then ∏ x ∈ s, f h x else ∏ x ∈ s, g h x
Full source 
@[to_additive (attr := simp)]
theorem prod_dite_irrel (p : Prop) [Decidable p] (s : Finset α) (f : p → α → β) (g : ¬p → α → β) :
    ∏ x ∈ s, (if h : p then f h x else g h x) =
      if h : p then ∏ x ∈ s, f h x else ∏ x ∈ s, g h x := by
  split_ifs with h <;> rfl
Conditional Product Equality with Dependent Functions
Informal description
Let $p$ be a decidable proposition, $s$ be a finite set of elements of type $\alpha$, and $f : p \to \alpha \to \beta$, $g : \neg p \to \alpha \to \beta$ be functions into a commutative monoid $\beta$. Then the product over $s$ of the function that evaluates to $f(h, x)$ if $h : p$ holds and $g(h, x)$ otherwise is equal to the product of $f(h, \cdot)$ over $s$ if $h : p$ holds, and the product of $g(h, \cdot)$ over $s$ otherwise. In symbols: \[ \prod_{x \in s} \left(\text{if } h : p \text{ then } f(h, x) \text{ else } g(h, x)\right) = \text{if } h : p \text{ then } \prod_{x \in s} f(h, x) \text{ else } \prod_{x \in s} g(h, x). \]
Finset.ite_prod_one theorem
(p : Prop) [Decidable p] (s : Finset α) (f : α → β) : (if p then (∏ x ∈ s, f x) else 1) = ∏ x ∈ s, if p then f x else 1
Full source 
@[to_additive]
theorem ite_prod_one (p : Prop) [Decidable p] (s : Finset α) (f : α → β) :
    (if p then (∏ x ∈ s, f x) else 1) = ∏ x ∈ s, if p then f x else 1 := by
  simp only [prod_ite_irrel, prod_const_one]
Conditional Product Identity: $\text{if } p \text{ then } \prod_{x \in s} f(x) \text{ else } 1 = \prod_{x \in s} \left(\text{if } p \text{ then } f(x) \text{ else } 1\right)$
Informal description
Let $p$ be a decidable proposition, $s$ be a finite set of elements of type $\alpha$, and $f : \alpha \to \beta$ be a function into a commutative monoid $\beta$. Then the conditional expression evaluating to the product $\prod_{x \in s} f(x)$ if $p$ holds and $1$ otherwise is equal to the product over $s$ of the function that evaluates to $f(x)$ if $p$ holds and $1$ otherwise. In symbols: \[ \text{if } p \text{ then } \prod_{x \in s} f(x) \text{ else } 1 = \prod_{x \in s} \left(\text{if } p \text{ then } f(x) \text{ else } 1\right). \]
Finset.ite_one_prod theorem
(p : Prop) [Decidable p] (s : Finset α) (f : α → β) : (if p then 1 else (∏ x ∈ s, f x)) = ∏ x ∈ s, if p then 1 else f x
Full source 
@[to_additive]
theorem ite_one_prod (p : Prop) [Decidable p] (s : Finset α) (f : α → β) :
    (if p then 1 else (∏ x ∈ s, f x)) = ∏ x ∈ s, if p then 1 else f x := by
  simp only [prod_ite_irrel, prod_const_one]
Conditional Product Identity: $\text{if } p \text{ then } 1 \text{ else } \prod_{x \in s} f(x) = \prod_{x \in s} \text{if } p \text{ then } 1 \text{ else } f(x)$
Informal description
Let $p$ be a decidable proposition, $s$ be a finite set of elements of type $\alpha$, and $f : \alpha \to \beta$ be a function into a commutative monoid $\beta$. Then the following equality holds: \[ \left(\text{if } p \text{ then } 1 \text{ else } \prod_{x \in s} f(x)\right) = \prod_{x \in s} \left(\text{if } p \text{ then } 1 \text{ else } f(x)\right). \]
Finset.nonempty_of_prod_ne_one theorem
(h : ∏ x ∈ s, f x ≠ 1) : s.Nonempty
Full source 
@[to_additive]
theorem nonempty_of_prod_ne_one (h : ∏ x ∈ s, f x∏ x ∈ s, f x ≠ 1) : s.Nonempty :=
  s.eq_empty_or_nonempty.elim (fun H => False.elim <| h <| H.symm ▸ prod_empty) id
Nonempty Set from Non-Identity Product: $\prod_{x \in s} f(x) \neq 1 \implies s \neq \emptyset$
Informal description
For any finite set $s$ and function $f$ mapping elements of $s$ to a commutative monoid, if the product $\prod_{x \in s} f(x)$ is not equal to the multiplicative identity $1$, then $s$ must be nonempty.
Finset.prod_range_zero theorem
(f : ℕ → β) : ∏ k ∈ range 0, f k = 1
Full source 
@[to_additive]
theorem prod_range_zero (f : ℕ → β) : ∏ k ∈ range 0, f k = 1 := by rw [range_zero, prod_empty]
Empty Product over Range Zero: $\prod_{k \in \text{range } 0} f(k) = 1$
Informal description
For any function $f \colon \mathbb{N} \to \beta$ where $\beta$ is a commutative monoid, the product of $f$ over the empty range (i.e., the finite set $\{0, \ldots, -1\}$) is equal to the multiplicative identity $1$: \[ \prod_{k \in \text{range } 0} f(k) = 1. \]
Finset.sum_filter_count_eq_countP theorem
[DecidableEq α] (p : α → Prop) [DecidablePred p] (l : List α) : ∑ x ∈ l.toFinset with p x, l.count x = l.countP p
Full source 
theorem sum_filter_count_eq_countP [DecidableEq α] (p : α → Prop) [DecidablePred p] (l : List α) :
    ∑ x ∈ l.toFinset with p x, l.count x = l.countP p := by
  simp [Finset.sum, sum_map_count_dedup_filter_eq_countP p l]
Sum of Filtered Counts Equals Predicate Count on List
Informal description
Let $\alpha$ be a type with decidable equality, $p : \alpha \to \mathrm{Prop}$ a decidable predicate, and $l$ a list of elements of $\alpha$. Then the sum of the counts of elements in $l$ that satisfy $p$ over the deduplicated set $l.\mathrm{toFinset}$ equals the count of elements in $l$ that satisfy $p$. In other words: \[ \sum_{x \in l.\mathrm{toFinset}, p x} \mathrm{count}_l(x) = \mathrm{countP}_l(p) \]
Finset.prod_mem_multiset theorem
[DecidableEq α] (m : Multiset α) (f : { x // x ∈ m } → β) (g : α → β) (hfg : ∀ x, f x = g x) : ∏ x : { x // x ∈ m }, f x = ∏ x ∈ m.toFinset, g x
Full source 
@[to_additive]
theorem prod_mem_multiset [DecidableEq α] (m : Multiset α) (f : { x // x ∈ m } → β) (g : α → β)
    (hfg : ∀ x, f x = g x) : ∏ x : { x // x ∈ m }, f x = ∏ x ∈ m.toFinset, g x := by
  refine prod_bij' (fun x _ ↦ x) (fun x hx ↦ ⟨x, Multiset.mem_toFinset.1 hx⟩) ?_ ?_ ?_ ?_ ?_ <;>
    simp [hfg]
Product Equality for Multiset Subtype and Deduplicated Finite Set
Informal description
Let $\alpha$ be a type with decidable equality, $m$ a multiset over $\alpha$, and $\beta$ a commutative monoid. Given two functions $f \colon \{x \mid x \in m\} \to \beta$ and $g \colon \alpha \to \beta$ such that $f(x) = g(x)$ for all $x \in m$, the product of $f$ over the subtype $\{x \mid x \in m\}$ is equal to the product of $g$ over the finite set obtained by removing duplicates from $m$: \[ \prod_{x \in \{x \mid x \in m\}} f(x) = \prod_{x \in m.\mathrm{toFinset}} g(x). \]
Finset.prod_induction theorem
{M : Type*} [CommMonoid M] (f : α → M) (p : M → Prop) (hom : ∀ a b, p a → p b → p (a * b)) (unit : p 1) (base : ∀ x ∈ s, p <| f x) : p <| ∏ x ∈ s, f x
Full source 
/-- To prove a property of a product, it suffices to prove that
the property is multiplicative and holds on factors. -/
@[to_additive "To prove a property of a sum, it suffices to prove that
the property is additive and holds on summands."]
theorem prod_induction {M : Type*} [CommMonoid M] (f : α → M) (p : M → Prop)
    (hom : ∀ a b, p a → p b → p (a * b)) (unit : p 1) (base : ∀ x ∈ s, p <| f x) :
    p <| ∏ x ∈ s, f x :=
  Multiset.prod_induction _ _ hom unit (Multiset.forall_mem_map_iff.mpr base)
Induction Principle for Products over Finite Sets
Informal description
Let $M$ be a commutative monoid, $s$ a finite set, and $f : \alpha \to M$ a function. Given a predicate $p : M \to \mathrm{Prop}$ such that: 1. $p$ is multiplicative: for all $a, b \in M$, if $p(a)$ and $p(b)$ hold, then $p(a \cdot b)$ holds, 2. $p(1)$ holds (where $1$ is the identity element of $M$), 3. For every $x \in s$, $p(f(x))$ holds, then the predicate $p$ holds for the product $\prod_{x \in s} f(x)$.
Finset.prod_induction_nonempty theorem
{M : Type*} [CommMonoid M] (f : α → M) (p : M → Prop) (hom : ∀ a b, p a → p b → p (a * b)) (nonempty : s.Nonempty) (base : ∀ x ∈ s, p <| f x) : p <| ∏ x ∈ s, f x
Full source 
/-- To prove a property of a product, it suffices to prove that
the property is multiplicative and holds on factors. -/
@[to_additive "To prove a property of a sum, it suffices to prove that
the property is additive and holds on summands."]
theorem prod_induction_nonempty {M : Type*} [CommMonoid M] (f : α → M) (p : M → Prop)
    (hom : ∀ a b, p a → p b → p (a * b)) (nonempty : s.Nonempty) (base : ∀ x ∈ s, p <| f x) :
    p <| ∏ x ∈ s, f x :=
  Multiset.prod_induction_nonempty p hom (by simp [nonempty_iff_ne_empty.mp nonempty])
    (Multiset.forall_mem_map_iff.mpr base)
Induction Principle for Products over Nonempty Finite Sets
Informal description
Let $M$ be a commutative monoid, $s$ a nonempty finite set, and $f : \alpha \to M$ a function. Given a predicate $p : M \to \mathrm{Prop}$ such that: 1. $p$ is multiplicative: for all $a, b \in M$, if $p(a)$ and $p(b)$ hold, then $p(a \cdot b)$ holds, 2. For every $x \in s$, $p(f(x))$ holds, then the predicate $p$ holds for the product $\prod_{x \in s} f(x)$.
Finset.prod_pow theorem
(s : Finset α) (n : ℕ) (f : α → β) : ∏ x ∈ s, f x ^ n = (∏ x ∈ s, f x) ^ n
Full source 
@[to_additive]
theorem prod_pow (s : Finset α) (n : ℕ) (f : α → β) : ∏ x ∈ s, f x ^ n = (∏ x ∈ s, f x) ^ n :=
  Multiset.prod_map_pow
Power of Product Equals Product of Powers in Commutative Monoids
Informal description
Let $s$ be a finite set, $n$ a natural number, and $f : \alpha \to \beta$ a function where $\beta$ is a commutative monoid. Then the product of $f(x)^n$ over all $x \in s$ is equal to the $n$-th power of the product of $f(x)$ over all $x \in s$, i.e., \[ \prod_{x \in s} f(x)^n = \left( \prod_{x \in s} f(x) \right)^n. \]
Finset.prod_dvd_prod_of_subset theorem
{ι M : Type*} [CommMonoid M] (s t : Finset ι) (f : ι → M) (h : s ⊆ t) : (∏ i ∈ s, f i) ∣ ∏ i ∈ t, f i
Full source 
theorem prod_dvd_prod_of_subset {ι M : Type*} [CommMonoid M] (s t : Finset ι) (f : ι → M)
    (h : s ⊆ t) : (∏ i ∈ s, f i) ∣ ∏ i ∈ t, f i :=
  Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map <| by simpa
Product Divisibility under Subset Inclusion in Commutative Monoids
Informal description
Let $s$ and $t$ be finite subsets of a type $\iota$ with $s \subseteq t$, and let $f : \iota \to M$ be a function where $M$ is a commutative monoid. Then the product $\prod_{i \in s} f(i)$ divides the product $\prod_{i \in t} f(i)$.
Finset.op_sum theorem
[AddCommMonoid β] {s : Finset α} (f : α → β) : op (∑ x ∈ s, f x) = ∑ x ∈ s, op (f x)
Full source 
/-- Moving to the opposite additive commutative monoid commutes with summing. -/
@[simp]
theorem op_sum [AddCommMonoid β] {s : Finset α} (f : α → β) :
    op (∑ x ∈ s, f x) = ∑ x ∈ s, op (f x) :=
  map_sum (opAddEquiv : β ≃+ βᵐᵒᵖ) _ _
Sum Commutes with Canonical Embedding into Multiplicative Opposite
Informal description
Let $\beta$ be an additive commutative monoid, $s$ a finite subset of a type $\alpha$, and $f : \alpha \to \beta$ a function. Then the canonical embedding into the multiplicative opposite of the sum of $f$ over $s$ equals the sum of the canonical embeddings of $f(x)$ for each $x \in s$: \[ \text{op}\left(\sum_{x \in s} f(x)\right) = \sum_{x \in s} \text{op}(f(x)). \]
Finset.unop_sum theorem
[AddCommMonoid β] {s : Finset α} (f : α → βᵐᵒᵖ) : unop (∑ x ∈ s, f x) = ∑ x ∈ s, unop (f x)
Full source 
@[simp]
theorem unop_sum [AddCommMonoid β] {s : Finset α} (f : α → βᵐᵒᵖ) :
    unop (∑ x ∈ s, f x) = ∑ x ∈ s, unop (f x) :=
  map_sum (opAddEquiv : β ≃+ βᵐᵒᵖ).symm _ _
Sum of Unary Operations Equals Unary Operation of Sum in Multiplicative Opposite
Informal description
Let $\beta$ be an additive commutative monoid, $s$ a finite subset of a type $\alpha$, and $f : \alpha \to \beta^\text{op}$ a function. Then the unary operation $\text{unop}$ applied to the sum $\sum_{x \in s} f(x)$ equals the sum $\sum_{x \in s} \text{unop}(f(x))$.
Finset.prod_inv_distrib theorem
: (∏ x ∈ s, (f x)⁻¹) = (∏ x ∈ s, f x)⁻¹
Full source 
@[to_additive (attr := simp)]
theorem prod_inv_distrib : (∏ x ∈ s, (f x)⁻¹) = (∏ x ∈ s, f x)⁻¹ :=
  Multiset.prod_map_inv
Inverse of Product Equals Product of Inverses in Commutative Division Monoids
Informal description
For any commutative division monoid $\beta$, finite set $s$ of a type $\alpha$, and function $f : \alpha \to \beta$, the product of inverses $\prod_{x \in s} (f(x))^{-1}$ equals the inverse of the product $(\prod_{x \in s} f(x))^{-1}$.
Finset.prod_div_distrib theorem
: ∏ x ∈ s, f x / g x = (∏ x ∈ s, f x) / ∏ x ∈ s, g x
Full source 
@[to_additive (attr := simp)]
theorem prod_div_distrib : ∏ x ∈ s, f x / g x = (∏ x ∈ s, f x) / ∏ x ∈ s, g x :=
  Multiset.prod_map_div
Product of Pointwise Division Equals Division of Products
Informal description
For any commutative division monoid $\beta$, finite set $s$ of type $\alpha$, and functions $f, g : \alpha \to \beta$, the product of the pointwise division $\prod_{x \in s} (f(x) / g(x))$ equals the division of the products $(\prod_{x \in s} f(x)) / (\prod_{x \in s} g(x))$.
Finset.prod_zpow theorem
(f : α → β) (s : Finset α) (n : ℤ) : ∏ a ∈ s, f a ^ n = (∏ a ∈ s, f a) ^ n
Full source 
@[to_additive]
theorem prod_zpow (f : α → β) (s : Finset α) (n : ℤ) : ∏ a ∈ s, f a ^ n = (∏ a ∈ s, f a) ^ n :=
  Multiset.prod_map_zpow
Power of Product Equals Product of Powers in Commutative Division Monoids
Informal description
For any commutative division monoid $\beta$, finite set $s$ of type $\alpha$, function $f : \alpha \to \beta$, and integer $n \in \mathbb{Z}$, the product of the $n$-th powers $\prod_{a \in s} f(a)^n$ equals the $n$-th power of the product $(\prod_{a \in s} f(a))^n$.
Finset.sum_nat_mod theorem
(s : Finset α) (n : ℕ) (f : α → ℕ) : (∑ i ∈ s, f i) % n = (∑ i ∈ s, f i % n) % n
Full source 
theorem sum_nat_mod (s : Finset α) (n : ℕ) (f : α → ℕ) :
    (∑ i ∈ s, f i) % n = (∑ i ∈ s, f i % n) % n :=
  (Multiset.sum_nat_mod _ _).trans <| by rw [Finset.sum, Multiset.map_map]; rfl
Modular Arithmetic of Finite Sums: $\left(\sum_i f(i)\right) \bmod n = \left(\sum_i (f(i) \bmod n)\right) \bmod n$
Informal description
For any finite set $s$ of type $\alpha$, natural number $n$, and function $f : \alpha \to \mathbb{N}$, the remainder of the sum $\sum_{i \in s} f(i)$ modulo $n$ is equal to the remainder of the sum $\sum_{i \in s} (f(i) \bmod n)$ modulo $n$. That is, \[ \left(\sum_{i \in s} f(i)\right) \bmod n = \left(\sum_{i \in s} (f(i) \bmod n)\right) \bmod n. \]
Finset.prod_nat_mod theorem
(s : Finset α) (n : ℕ) (f : α → ℕ) : (∏ i ∈ s, f i) % n = (∏ i ∈ s, f i % n) % n
Full source 
theorem prod_nat_mod (s : Finset α) (n : ℕ) (f : α → ℕ) :
    (∏ i ∈ s, f i) % n = (∏ i ∈ s, f i % n) % n :=
  (Multiset.prod_nat_mod _ _).trans <| by rw [Finset.prod, Multiset.map_map]; rfl
Modular Arithmetic of Finite Products: $\left(\prod_i f(i)\right) \bmod n = \left(\prod_i (f(i) \bmod n)\right) \bmod n$
Informal description
For any finite set $s$ of type $\alpha$, natural number $n$, and function $f : \alpha \to \mathbb{N}$, the remainder of the product $\prod_{i \in s} f(i)$ modulo $n$ is equal to the remainder of the product $\prod_{i \in s} (f(i) \bmod n)$ modulo $n$. That is, \[ \left(\prod_{i \in s} f(i)\right) \bmod n = \left(\prod_{i \in s} (f(i) \bmod n)\right) \bmod n. \]
Finset.sum_int_mod theorem
(s : Finset α) (n : ℤ) (f : α → ℤ) : (∑ i ∈ s, f i) % n = (∑ i ∈ s, f i % n) % n
Full source 
theorem sum_int_mod (s : Finset α) (n : ℤ) (f : α → ℤ) :
    (∑ i ∈ s, f i) % n = (∑ i ∈ s, f i % n) % n :=
  (Multiset.sum_int_mod _ _).trans <| by rw [Finset.sum, Multiset.map_map]; rfl
Modular Arithmetic of Finite Sums: $\left(\sum_i f(i)\right) \bmod n = \left(\sum_i (f(i) \bmod n)\right) \bmod n$
Informal description
For any finite set $s$ of type $\alpha$, integer $n$, and function $f : \alpha \to \mathbb{Z}$, the remainder of the sum $\sum_{i \in s} f(i)$ modulo $n$ is equal to the remainder of the sum $\sum_{i \in s} (f(i) \bmod n)$ modulo $n$. That is, \[ \left(\sum_{i \in s} f(i)\right) \bmod n = \left(\sum_{i \in s} (f(i) \bmod n)\right) \bmod n. \]
Finset.prod_int_mod theorem
(s : Finset α) (n : ℤ) (f : α → ℤ) : (∏ i ∈ s, f i) % n = (∏ i ∈ s, f i % n) % n
Full source 
theorem prod_int_mod (s : Finset α) (n : ℤ) (f : α → ℤ) :
    (∏ i ∈ s, f i) % n = (∏ i ∈ s, f i % n) % n :=
  (Multiset.prod_int_mod _ _).trans <| by rw [Finset.prod, Multiset.map_map]; rfl
Modular Arithmetic of Finite Products over Integers: $\left(\prod_i f(i)\right) \bmod n = \left(\prod_i (f(i) \bmod n)\right) \bmod n$
Informal description
For any finite set $s$ of type $\alpha$, integer $n$, and function $f : \alpha \to \mathbb{Z}$, the remainder of the product $\prod_{i \in s} f(i)$ modulo $n$ is equal to the remainder of the product $\prod_{i \in s} (f(i) \bmod n)$ modulo $n$. That is, \[ \left(\prod_{i \in s} f(i)\right) \bmod n = \left(\prod_{i \in s} (f(i) \bmod n)\right) \bmod n. \]
Fintype.prod_bijective theorem
(e : ι → κ) (he : e.Bijective) (f : ι → α) (g : κ → α) (h : ∀ x, f x = g (e x)) : ∏ x, f x = ∏ x, g x
Full source 
/-- `Fintype.prod_bijective` is a variant of `Finset.prod_bij` that accepts `Function.Bijective`.

See `Function.Bijective.prod_comp` for a version without `h`. -/
@[to_additive "`Fintype.sum_bijective` is a variant of `Finset.sum_bij` that accepts
`Function.Bijective`.

See `Function.Bijective.sum_comp` for a version without `h`. "]
lemma prod_bijective (e : ι → κ) (he : e.Bijective) (f : ι → α) (g : κ → α)
    (h : ∀ x, f x = g (e x)) : ∏ x, f x = ∏ x, g x :=
  prod_equiv (.ofBijective e he) (by simp) (by simp [h])
Product Equality under Bijection: $\prod_{x} f(x) = \prod_{x} g(x)$
Informal description
Let $\iota$ and $\kappa$ be finite types, and let $\alpha$ be a commutative monoid. Given a bijective function $e : \iota \to \kappa$ and functions $f : \iota \to \alpha$ and $g : \kappa \to \alpha$ such that for every $x \in \iota$, $f(x) = g(e(x))$, then the products satisfy \[ \prod_{x \in \iota} f(x) = \prod_{x \in \kappa} g(x). \]
Fintype.prod_equiv theorem
(e : ι ≃ κ) (f : ι → α) (g : κ → α) (h : ∀ x, f x = g (e x)) : ∏ x, f x = ∏ x, g x
Full source 
/-- `Fintype.prod_equiv` is a specialization of `Finset.prod_bij` that
automatically fills in most arguments.

See `Equiv.prod_comp` for a version without `h`.
-/
@[to_additive "`Fintype.sum_equiv` is a specialization of `Finset.sum_bij` that
automatically fills in most arguments.

See `Equiv.sum_comp` for a version without `h`."]
lemma prod_equiv (e : ι ≃ κ) (f : ι → α) (g : κ → α) (h : ∀ x, f x = g (e x)) :
    ∏ x, f x = ∏ x, g x := prod_bijective _ e.bijective _ _ h
Product Equality under Type Equivalence: $\prod_{x} f(x) = \prod_{x} g(x)$
Informal description
Let $\iota$ and $\kappa$ be finite types, and let $\alpha$ be a commutative monoid. Given an equivalence (bijection) $e : \iota \simeq \kappa$ and functions $f : \iota \to \alpha$ and $g : \kappa \to \alpha$ such that for every $x \in \iota$, $f(x) = g(e(x))$, then the products satisfy \[ \prod_{x \in \iota} f(x) = \prod_{x \in \kappa} g(x). \]
Function.Bijective.prod_comp theorem
{e : ι → κ} (he : e.Bijective) (g : κ → α) : ∏ i, g (e i) = ∏ i, g i
Full source 
@[to_additive]
lemma _root_.Function.Bijective.prod_comp {e : ι → κ} (he : e.Bijective) (g : κ → α) :
    ∏ i, g (e i) = ∏ i, g i := prod_bijective _ he _ _ fun _ ↦ rfl
Product Equality under Bijective Composition: $\prod_{i} g(e(i)) = \prod_{i} g(i)$
Informal description
Let $\iota$ and $\kappa$ be finite types, and let $\alpha$ be a commutative monoid. Given a bijective function $e : \iota \to \kappa$ and a function $g : \kappa \to \alpha$, the product of $g$ composed with $e$ over $\iota$ is equal to the product of $g$ over $\kappa$, i.e., \[ \prod_{i \in \iota} g(e(i)) = \prod_{i \in \kappa} g(i). \]
Equiv.prod_comp theorem
(e : ι ≃ κ) (g : κ → α) : ∏ i, g (e i) = ∏ i, g i
Full source 
@[to_additive]
lemma _root_.Equiv.prod_comp (e : ι ≃ κ) (g : κ → α) : ∏ i, g (e i) = ∏ i, g i :=
  prod_equiv e _ _ fun _ ↦ rfl
Product Invariance under Type Equivalence: $\prod_{i} g(e(i)) = \prod_{i} g(i)$
Informal description
Let $\iota$ and $\kappa$ be finite types, and let $\alpha$ be a commutative monoid. Given an equivalence (bijection) $e : \iota \simeq \kappa$ and a function $g : \kappa \to \alpha$, the product of $g \circ e$ over $\iota$ is equal to the product of $g$ over $\kappa$, i.e., \[ \prod_{i \in \iota} g(e(i)) = \prod_{i \in \kappa} g(i). \]
Fintype.prod_empty theorem
{α β : Type*} [CommMonoid β] [IsEmpty α] [Fintype α] (f : α → β) : ∏ x : α, f x = 1
Full source 
@[to_additive]
theorem prod_empty {α β : Type*} [CommMonoid β] [IsEmpty α] [Fintype α] (f : α → β) :
    ∏ x : α, f x = 1 :=
  Finset.prod_of_isEmpty _
Empty Product Equals One: $\prod_{x : \alpha} f(x) = 1$ when $\alpha$ is empty
Informal description
For any empty type $\alpha$ (i.e., a type with no elements) and any commutative monoid $\beta$, the product $\prod_{x : \alpha} f(x)$ over all elements of $\alpha$ is equal to the multiplicative identity $1$ in $\beta$.
Finset.prod_attach_univ theorem
[Fintype ι] (f : { i // i ∈ @univ ι _ } → α) : ∏ i ∈ univ.attach, f i = ∏ i, f ⟨i, mem_univ _⟩
Full source 
@[to_additive (attr := simp)]
lemma prod_attach_univ [Fintype ι] (f : {i // i ∈ @univ ι _} → α) :
    ∏ i ∈ univ.attach, f i = ∏ i, f ⟨i, mem_univ _⟩ :=
  Fintype.prod_equiv (Equiv.subtypeUnivEquiv mem_univ) _ _ <| by simp
Product Equality over Attached Universal Finite Set: $\prod_{i \in \text{univ.attach}} f(i) = \prod_{i \in \iota} f(i)$
Informal description
Let $\iota$ be a finite type and $\alpha$ a commutative monoid. For any function $f$ defined on the subtype $\{i \in \iota \mid i \in \text{univ}\}$, the product $\prod_{i \in \text{univ.attach}} f(i)$ is equal to the product $\prod_{i \in \iota} f(\langle i, \text{mem\_univ } i \rangle)$, where $\text{univ.attach}$ is the finite set of elements of $\iota$ paired with their membership proofs in $\text{univ}$.
Finset.prod_erase_attach theorem
[DecidableEq ι] {s : Finset ι} (f : ι → α) (i : ↑s) : ∏ j ∈ s.attach.erase i, f ↑j = ∏ j ∈ s.erase ↑i, f j
Full source 
@[to_additive]
theorem prod_erase_attach [DecidableEq ι] {s : Finset ι} (f : ι → α) (i : ↑s) :
    ∏ j ∈ s.attach.erase i, f ↑j = ∏ j ∈ s.erase ↑i, f j := by
  rw [← Function.Embedding.coe_subtype, ← prod_map]
  simp [attach_map_val]
Product Equality over Erased Attached Set: $\prod_{j \in s.\text{attach} \setminus \{i\}} f(j) = \prod_{j \in s \setminus \{i\}} f(j)$
Informal description
Let $\iota$ be a type with decidable equality, $s$ a finite subset of $\iota$, and $f : \iota \to \alpha$ a function where $\alpha$ is a commutative monoid. For any element $i$ in the attached set $\{x \in \iota \mid x \in s\}$, the product of $f$ over the erased attached set $s.\text{attach} \setminus \{i\}$ equals the product of $f$ over the erased original set $s \setminus \{\text{val}(i)\}$. In symbols: \[ \prod_{j \in s.\text{attach} \setminus \{i\}} f(j) = \prod_{j \in s \setminus \{\text{val}(i)\}} f(j). \]
Multiset.card_sum theorem
(s : Finset ι) (f : ι → Multiset α) : card (∑ i ∈ s, f i) = ∑ i ∈ s, card (f i)
Full source 
@[simp]
lemma card_sum (s : Finset ι) (f : ι → Multiset α) : card (∑ i ∈ s, f i) = ∑ i ∈ s, card (f i) :=
  map_sum cardHom ..
Cardinality of Sum of Multisets Equals Sum of Cardinalities
Informal description
For any finite set $s$ indexed by type $\iota$ and any function $f \colon \iota \to \text{Multiset } \alpha$, the cardinality of the sum of multisets $\sum_{i \in s} f(i)$ is equal to the sum of the cardinalities $\sum_{i \in s} \text{card}(f(i))$.
Multiset.disjoint_list_sum_left theorem
{a : Multiset α} {l : List (Multiset α)} : Disjoint l.sum a ↔ ∀ b ∈ l, Disjoint b a
Full source 
theorem disjoint_list_sum_left {a : Multiset α} {l : List (Multiset α)} :
    DisjointDisjoint l.sum a ↔ ∀ b ∈ l, Disjoint b a := by
  induction l with
  | nil =>
    simp only [zero_disjoint, List.not_mem_nil, IsEmpty.forall_iff, forall_const, List.sum_nil]
  | cons b bs ih =>
    simp_rw [List.sum_cons, disjoint_add_left, List.mem_cons, forall_eq_or_imp]
    simp [and_congr_left_iff, ih]
Disjointness of Sum of Multisets from a Multiset
Informal description
For a multiset $a$ and a list $l$ of multisets over a type $\alpha$, the sum of the multisets in $l$ is disjoint from $a$ if and only if every multiset $b$ in $l$ is disjoint from $a$. In symbols: \[ \text{Disjoint}\left(\sum_{b \in l} b, a\right) \leftrightarrow \forall b \in l, \text{Disjoint}(b, a). \]
Multiset.disjoint_list_sum_right theorem
{a : Multiset α} {l : List (Multiset α)} : Disjoint a l.sum ↔ ∀ b ∈ l, Disjoint a b
Full source 
theorem disjoint_list_sum_right {a : Multiset α} {l : List (Multiset α)} :
    DisjointDisjoint a l.sum ↔ ∀ b ∈ l, Disjoint a b := by
  simpa only [disjoint_comm (a := a)] using disjoint_list_sum_left
Disjointness of a Multiset from Sum of List of Multisets
Informal description
For a multiset $a$ and a list $l$ of multisets over a type $\alpha$, the multiset $a$ is disjoint from the sum of the multisets in $l$ if and only if $a$ is disjoint from every multiset $b$ in $l$. In symbols: \[ \text{Disjoint}\left(a, \sum_{b \in l} b\right) \leftrightarrow \forall b \in l, \text{Disjoint}(a, b). \]
Multiset.disjoint_sum_left theorem
{a : Multiset α} {i : Multiset (Multiset α)} : Disjoint i.sum a ↔ ∀ b ∈ i, Disjoint b a
Full source 
theorem disjoint_sum_left {a : Multiset α} {i : Multiset (Multiset α)} :
    DisjointDisjoint i.sum a ↔ ∀ b ∈ i, Disjoint b a :=
  Quotient.inductionOn i fun l => by
    rw [quot_mk_to_coe, Multiset.sum_coe]
    exact disjoint_list_sum_left
Disjointness of Sum of Multisets from a Multiset (Multiset Version)
Informal description
For a multiset $a$ and a multiset $i$ of multisets over a type $\alpha$, the sum of the multisets in $i$ is disjoint from $a$ if and only if every multiset $b$ in $i$ is disjoint from $a$. In symbols: \[ \text{Disjoint}\left(\sum_{b \in i} b, a\right) \leftrightarrow \forall b \in i, \text{Disjoint}(b, a). \]
Multiset.disjoint_sum_right theorem
{a : Multiset α} {i : Multiset (Multiset α)} : Disjoint a i.sum ↔ ∀ b ∈ i, Disjoint a b
Full source 
theorem disjoint_sum_right {a : Multiset α} {i : Multiset (Multiset α)} :
    DisjointDisjoint a i.sum ↔ ∀ b ∈ i, Disjoint a b := by
  simpa only [disjoint_comm (a := a)] using disjoint_sum_left
Disjointness of a Multiset from Sum of Multiset of Multisets
Informal description
For a multiset $a$ and a multiset $i$ of multisets over a type $\alpha$, the multiset $a$ is disjoint from the sum of the multisets in $i$ if and only if $a$ is disjoint from every multiset $b$ in $i$. In symbols: \[ \text{Disjoint}(a, \sum_{b \in i} b) \leftrightarrow \forall b \in i, \text{Disjoint}(a, b). \]
Multiset.disjoint_finset_sum_left theorem
{β : Type*} {i : Finset β} {f : β → Multiset α} {a : Multiset α} : Disjoint (i.sum f) a ↔ ∀ b ∈ i, Disjoint (f b) a
Full source 
theorem disjoint_finset_sum_left {β : Type*} {i : Finset β} {f : β → Multiset α} {a : Multiset α} :
    DisjointDisjoint (i.sum f) a ↔ ∀ b ∈ i, Disjoint (f b) a := by
  convert @disjoint_sum_left _ a (map f i.val)
  simp [and_congr_left_iff]
Disjointness of Finite Sum of Multisets from a Multiset: $\text{Disjoint}(\sum_{b \in i} f(b), a) \leftrightarrow \forall b \in i, \text{Disjoint}(f(b), a)$
Informal description
For any finite set $i$ over a type $\beta$, a function $f : \beta \to \text{Multiset} \alpha$, and a multiset $a$ over $\alpha$, the sum of the multisets $\sum_{b \in i} f(b)$ is disjoint from $a$ if and only if for every element $b$ in $i$, the multiset $f(b)$ is disjoint from $a$. In symbols: \[ \text{Disjoint}\left(\sum_{b \in i} f(b), a\right) \leftrightarrow \forall b \in i, \text{Disjoint}(f(b), a). \]
Multiset.disjoint_finset_sum_right theorem
{β : Type*} {i : Finset β} {f : β → Multiset α} {a : Multiset α} : Disjoint a (i.sum f) ↔ ∀ b ∈ i, Disjoint a (f b)
Full source 
theorem disjoint_finset_sum_right {β : Type*} {i : Finset β} {f : β → Multiset α}
    {a : Multiset α} : DisjointDisjoint a (i.sum f) ↔ ∀ b ∈ i, Disjoint a (f b) := by
  simpa only [disjoint_comm] using disjoint_finset_sum_left
Disjointness of a Multiset from Finite Sum of Multisets: $\text{Disjoint}(a, \sum_{b \in i} f(b)) \leftrightarrow \forall b \in i, \text{Disjoint}(a, f(b))$
Informal description
For any finite set $i$ over a type $\beta$, a function $f : \beta \to \text{Multiset} \alpha$, and a multiset $a$ over $\alpha$, the multiset $a$ is disjoint from the sum of the multisets $\sum_{b \in i} f(b)$ if and only if for every element $b$ in $i$, the multiset $a$ is disjoint from $f(b)$. In symbols: \[ \text{Disjoint}\left(a, \sum_{b \in i} f(b)\right) \leftrightarrow \forall b \in i, \text{Disjoint}(a, f(b)). \]
Multiset.count_sum' theorem
{s : Finset β} {a : α} {f : β → Multiset α} : count a (∑ x ∈ s, f x) = ∑ x ∈ s, count a (f x)
Full source 
theorem count_sum' {s : Finset β} {a : α} {f : β → Multiset α} :
    count a (∑ x ∈ s, f x) = ∑ x ∈ s, count a (f x) := by
  dsimp only [Finset.sum]
  rw [count_sum]
Count-Sum Formula for Multisets: $\text{count}(a, \sum_{x \in s} f(x)) = \sum_{x \in s} \text{count}(a, f(x))$
Informal description
For any finite set $s$ over a type $\beta$, an element $a$ of type $\alpha$, and a function $f : \beta \to \text{Multiset} \alpha$, the multiplicity of $a$ in the sum of multisets $\sum_{x \in s} f(x)$ is equal to the sum over $s$ of the multiplicities of $a$ in each $f(x)$. In symbols: \[ \text{count}(a, \sum_{x \in s} f(x)) = \sum_{x \in s} \text{count}(a, f(x)). \]
Multiset.toFinset_prod_dvd_prod theorem
[CommMonoid α] (S : Multiset α) : S.toFinset.prod id ∣ S.prod
Full source 
theorem toFinset_prod_dvd_prod [CommMonoid α] (S : Multiset α) : S.toFinset.prod id ∣ S.prod := by
  rw [Finset.prod_eq_multiset_prod]
  refine Multiset.prod_dvd_prod_of_le ?_
  simp [Multiset.dedup_le S]
Product of Deduplicated Multiset Divides Original Product: $\prod_{\operatorname{toFinset}(S)} x \mid \prod_S x$
Informal description
For any multiset $S$ over a commutative monoid $\alpha$, the product of the elements in the finite set obtained by removing duplicates from $S$ divides the product of all elements in $S$. In symbols: $$\prod_{x \in \operatorname{toFinset}(S)} x \ \Big| \ \prod_{x \in S} x.$$
Units.coe_prod theorem
{M : Type*} [CommMonoid M] (f : α → Mˣ) (s : Finset α) : (↑(∏ i ∈ s, f i) : M) = ∏ i ∈ s, (f i : M)
Full source 
@[simp, norm_cast]
theorem Units.coe_prod {M : Type*} [CommMonoid M] (f : α → Mˣ) (s : Finset α) :
    (↑(∏ i ∈ s, f i) : M) = ∏ i ∈ s, (f i : M) :=
  map_prod (Units.coeHom M) _ _
Compatibility of Unit Product with Underlying Monoid Product: $\left(\prod_{i \in s} f(i)\right)_M = \prod_{i \in s} (f(i))_M$
Informal description
Let $M$ be a commutative monoid and $f : \alpha \to M^\times$ a function from a type $\alpha$ to the group of units of $M$. For any finite subset $s \subseteq \alpha$, the underlying element in $M$ of the product $\prod_{i \in s} f(i)$ (computed in $M^\times$) is equal to the product $\prod_{i \in s} f(i)$ (computed in $M$). In symbols: \[ \left(\prod_{i \in s} f(i)\right)_{\text{in } M} = \prod_{i \in s} (f(i))_{\text{in } M}. \]
ofMul_list_prod theorem
(s : List α) : ofMul s.prod = (s.map ofMul).sum
Full source 
@[simp]
theorem ofMul_list_prod (s : List α) : ofMul s.prod = (s.map ofMul).sum := by simp [ofMul]; rfl
Product-to-Sum Conversion via Additive Type Tag
Informal description
For any list $s$ of elements in a monoid $\alpha$, the image of the product of $s$ under the equivalence $\text{Additive.ofMul} : \alpha \simeq \text{Additive }\alpha$ is equal to the sum of the list obtained by applying $\text{Additive.ofMul}$ to each element of $s$. In symbols: $$\text{Additive.ofMul}\left(\prod_{x \in s} x\right) = \sum_{x \in s} \text{Additive.ofMul}(x).$$
toMul_list_sum theorem
(s : List (Additive α)) : s.sum.toMul = (s.map toMul).prod
Full source 
@[simp]
theorem toMul_list_sum (s : List (Additive α)) : s.sum.toMul = (s.map toMul).prod := by
  simp [toMul, ofMul]; rfl
Sum-to-Product Conversion for Additive Type Tag
Informal description
For any list `s` of elements in the additive type tag `Additive α`, the multiplicative interpretation of the sum of `s` is equal to the product of the multiplicative interpretations of the elements in `s`. In other words, if we convert each element of `s` back to its original multiplicative form and then take their product, it equals the conversion of the sum of `s` back to the multiplicative form.
ofAdd_list_prod theorem
(s : List α) : ofAdd s.sum = (s.map ofAdd).prod
Full source 
@[simp]
theorem ofAdd_list_prod (s : List α) : ofAdd s.sum = (s.map ofAdd).prod := by simp [ofAdd]; rfl
Sum-to-Product Conversion under Multiplicative Embedding for Lists
Informal description
For any list $s$ of elements of type $\alpha$, the image of the sum of $s$ under the embedding $\text{ofAdd} : \alpha \to \text{Multiplicative}\,\alpha$ is equal to the product of the list obtained by applying $\text{ofAdd}$ to each element of $s$.
toAdd_list_sum theorem
(s : List (Multiplicative α)) : s.prod.toAdd = (s.map toAdd).sum
Full source 
@[simp]
theorem toAdd_list_sum (s : List (Multiplicative α)) : s.prod.toAdd = (s.map toAdd).sum := by
  simp [toAdd, ofAdd]; rfl
Additive Projection of Multiplicative Product Equals Sum of Projections
Informal description
For any list $s$ of elements in the multiplicative type tag $\text{Multiplicative}\,\alpha$, the additive projection of the product of $s$ is equal to the sum of the additive projections of the elements in $s$. In other words, if $\text{toAdd} : \text{Multiplicative}\,\alpha \to \alpha$ is the projection map, then: \[ \text{toAdd}\left(\prod_{x \in s} x\right) = \sum_{x \in s} \text{toAdd}(x). \]
ofMul_multiset_prod theorem
(s : Multiset α) : ofMul s.prod = (s.map ofMul).sum
Full source 
@[simp]
theorem ofMul_multiset_prod (s : Multiset α) : ofMul s.prod = (s.map ofMul).sum := by
  simp [ofMul]; rfl
Product-to-Sum Conversion under Additive Embedding for Multisets
Informal description
For any multiset $s$ over a commutative monoid $\alpha$, the image of the product of $s$ under the embedding $\text{ofMul} : \alpha \to \text{Additive}\,\alpha$ is equal to the sum of the multiset obtained by applying $\text{ofMul}$ to each element of $s$. In other words: \[ \text{ofMul}\left(\prod_{x \in s} x\right) = \sum_{x \in s} \text{ofMul}(x). \]
toMul_multiset_sum theorem
(s : Multiset (Additive α)) : s.sum.toMul = (s.map toMul).prod
Full source 
@[simp]
theorem toMul_multiset_sum (s : Multiset (Additive α)) : s.sum.toMul = (s.map toMul).prod := by
  simp [toMul, ofMul]; rfl
Multiplicative Projection of Additive Sum Equals Product of Projections
Informal description
For any multiset $s$ over the additive type tag $\text{Additive}\,\alpha$, the multiplicative projection of the sum of $s$ is equal to the product of the multiplicative projections of the elements in $s$. In other words, if $\text{toMul} : \text{Additive}\,\alpha \to \alpha$ is the projection map, then: \[ \text{toMul}\left(\sum_{x \in s} x\right) = \prod_{x \in s} \text{toMul}(x). \]
ofMul_prod theorem
(s : Finset ι) (f : ι → α) : ofMul (∏ i ∈ s, f i) = ∑ i ∈ s, ofMul (f i)
Full source 
@[simp]
theorem ofMul_prod (s : Finset ι) (f : ι → α) : ofMul (∏ i ∈ s, f i) = ∑ i ∈ s, ofMul (f i) :=
  rfl
Conversion of Product to Sum via Additive Structure
Informal description
Let $s$ be a finite set indexed by $ι$ and $f : ι \to α$ a function. Then the additive version of the product $\prod_{i \in s} f(i)$ equals the sum $\sum_{i \in s} \text{ofMul}(f(i))$, where $\text{ofMul}$ is the conversion from multiplicative to additive structure.
toMul_sum theorem
(s : Finset ι) (f : ι → Additive α) : (∑ i ∈ s, f i).toMul = ∏ i ∈ s, (f i).toMul
Full source 
@[simp]
theorem toMul_sum (s : Finset ι) (f : ι → Additive α) :
    (∑ i ∈ s, f i).toMul = ∏ i ∈ s, (f i).toMul :=
  rfl
Conversion of Sum to Product via Additive-Multiplicative Equivalence
Informal description
Let $s$ be a finite set indexed by $\iota$, and let $f : \iota \to \text{Additive }\alpha$ be a function. Then the conversion of the sum $\sum_{i \in s} f(i)$ back to the multiplicative structure equals the product $\prod_{i \in s} f(i).\text{toMul}$, where $\text{toMul}$ is the bijection from $\text{Additive }\alpha$ to $\alpha$.
ofAdd_multiset_prod theorem
(s : Multiset α) : ofAdd s.sum = (s.map ofAdd).prod
Full source 
@[simp]
theorem ofAdd_multiset_prod (s : Multiset α) : ofAdd s.sum = (s.map ofAdd).prod := by
  simp [ofAdd]; rfl
Equivalence of Sum and Product under Multiplicative Type Tag: $\mathrm{ofAdd}(\sum s) = \prod (\mathrm{map}\,\mathrm{ofAdd}\,s)$
Informal description
Let $s$ be a multiset over an additive commutative monoid $\alpha$. Then the image of the sum of $s$ under the embedding $\mathrm{ofAdd} : \alpha \to \mathrm{Multiplicative}\,\alpha$ is equal to the product of the multiset obtained by applying $\mathrm{ofAdd}$ to each element of $s$. In other words, $\mathrm{ofAdd}(\sum s) = \prod (\mathrm{map}\,\mathrm{ofAdd}\,s)$.
toAdd_multiset_sum theorem
(s : Multiset (Multiplicative α)) : s.prod.toAdd = (s.map toAdd).sum
Full source 
@[simp]
theorem toAdd_multiset_sum (s : Multiset (Multiplicative α)) :
    s.prod.toAdd = (s.map toAdd).sum := by
  simp [toAdd, ofAdd]; rfl
Additive Projection of Product Equals Sum of Projections for Multiplicative Multisets
Informal description
For any multiset $s$ over the multiplicative type tag $\text{Multiplicative}\,\alpha$, the additive projection of the product of $s$ is equal to the sum of the additive projections of its elements, i.e., $\text{toAdd}(\prod s) = \sum (\text{map toAdd}\, s)$.
ofAdd_sum theorem
(s : Finset ι) (f : ι → α) : ofAdd (∑ i ∈ s, f i) = ∏ i ∈ s, ofAdd (f i)
Full source 
@[simp]
theorem ofAdd_sum (s : Finset ι) (f : ι → α) : ofAdd (∑ i ∈ s, f i) = ∏ i ∈ s, ofAdd (f i) :=
  rfl
Equivalence between additive sum and multiplicative product via $\text{ofAdd}$
Informal description
Let $α$ be an additive commutative monoid and let $s$ be a finite set indexed by $ι$. For any function $f : ι \to α$, the image of the sum $\sum_{i \in s} f(i)$ under the equivalence $\text{ofAdd} : α \simeq \text{Multiplicative}\,α$ is equal to the product $\prod_{i \in s} \text{ofAdd}(f(i))$ in the multiplicative commutative monoid $\text{Multiplicative}\,α$.
toAdd_prod theorem
(s : Finset ι) (f : ι → Multiplicative α) : (∏ i ∈ s, f i).toAdd = ∑ i ∈ s, (f i).toAdd
Full source 
@[simp]
theorem toAdd_prod (s : Finset ι) (f : ι → Multiplicative α) :
    (∏ i ∈ s, f i).toAdd = ∑ i ∈ s, (f i).toAdd :=
  rfl
Additive Projection of Product Equals Sum of Projections
Informal description
Let $s$ be a finite set indexed by $\iota$, and let $f : \iota \to \text{Multiplicative}\,\alpha$ be a function. Then the additive projection of the product $\prod_{i \in s} f(i)$ is equal to the sum $\sum_{i \in s} f(i).\text{toAdd}$.