Mathlib.Algebra.BigOperators.Pi

Pi.list_prod_apply theorem

 {α : Type*} {β : α → Type*} [∀ a, Monoid (β a)] (a : α) (l : List (∀ a, β a)) :
  l.prod a = (l.map fun f : ∀ a, β a ↦ f a).prod

Full source

@[to_additive]
theorem list_prod_apply {α : Type*} {β : α → Type*} [∀ a, Monoid (β a)] (a : α)
    (l : List (∀ a, β a)) : l.prod a = (l.map fun f : ∀ a, β a ↦ f a).prod :=
  map_list_prod (evalMonoidHom β a) _

Evaluation of List Product in Function Space

Informal description

Let $\alpha$ be a type and for each $a \in \alpha$, let $\beta(a)$ be a monoid. For any fixed $a \in \alpha$ and any list $l$ of functions from $\alpha$ to $\prod_{a \in \alpha} \beta(a)$, the evaluation of the product of $l$ at $a$ is equal to the product of the evaluations of the functions in $l$ at $a$. In other words, \[ \left(\prod_{f \in l} f\right)(a) = \prod_{f \in l} f(a). \]

Pi.multiset_prod_apply theorem

 {α : Type*} {β : α → Type*} [∀ a, CommMonoid (β a)] (a : α) (s : Multiset (∀ a, β a)) :
  s.prod a = (s.map fun f : ∀ a, β a ↦ f a).prod

Full source

@[to_additive]
theorem multiset_prod_apply {α : Type*} {β : α → Type*} [∀ a, CommMonoid (β a)] (a : α)
    (s : Multiset (∀ a, β a)) : s.prod a = (s.map fun f : ∀ a, β a ↦ f a).prod :=
  (evalMonoidHom β a).map_multiset_prod _

Evaluation of Multiset Product in Function Space

Informal description

Let $\alpha$ be a type, and for each $a \in \alpha$, let $\beta(a)$ be a commutative monoid. For any fixed $a \in \alpha$ and any multiset $s$ of functions from $\alpha$ to $\prod_{a \in \alpha} \beta(a)$, the evaluation of the product of $s$ at $a$ is equal to the product of the evaluations of the functions in $s$ at $a$. In other words, \[ \left(\prod_{f \in s} f\right)(a) = \prod_{f \in s} f(a). \]

Finset.prod_apply theorem

 {α : Type*} {β : α → Type*} {γ} [∀ a, CommMonoid (β a)] (a : α) (s : Finset γ) (g : γ → ∀ a, β a) :
  (∏ c ∈ s, g c) a = ∏ c ∈ s, g c a

Full source

@[to_additive (attr := simp)]
theorem Finset.prod_apply {α : Type*} {β : α → Type*} {γ} [∀ a, CommMonoid (β a)] (a : α)
    (s : Finset γ) (g : γ → ∀ a, β a) : (∏ c ∈ s, g c) a = ∏ c ∈ s, g c a :=
  map_prod (Pi.evalMonoidHom β a) _ _

Evaluation of Finite Product in Function Space

Informal description

Let $\alpha$ be a type, and for each $a \in \alpha$, let $\beta(a)$ be a commutative monoid. For any fixed $a \in \alpha$, any finite set $s$ (of type $\gamma$), and any function $g \colon \gamma \to \prod_{a \in \alpha} \beta(a)$, the evaluation at $a$ of the product of $g$ over $s$ is equal to the product over $s$ of the evaluations $g(c)(a)$. In other words, \[ \left(\prod_{c \in s} g(c)\right)(a) = \prod_{c \in s} g(c)(a). \]

Finset.prod_fn theorem

 {α : Type*} {β : α → Type*} {γ} [∀ a, CommMonoid (β a)] (s : Finset γ) (g : γ → ∀ a, β a) :
  ∏ c ∈ s, g c = fun a ↦ ∏ c ∈ s, g c a

Full source

/-- An 'unapplied' analogue of `Finset.prod_apply`. -/
@[to_additive "An 'unapplied' analogue of `Finset.sum_apply`."]
theorem Finset.prod_fn {α : Type*} {β : α → Type*} {γ} [∀ a, CommMonoid (β a)] (s : Finset γ)
    (g : γ → ∀ a, β a) : ∏ c ∈ s, g c = fun a ↦ ∏ c ∈ s, g c a :=
  funext fun _ ↦ Finset.prod_apply _ _ _

Product of Functions as Pointwise Product

Informal description

Let $\alpha$ be a type, and for each $a \in \alpha$, let $\beta(a)$ be a commutative monoid. For any finite set $s$ (of type $\gamma$) and any function $g \colon \gamma \to \prod_{a \in \alpha} \beta(a)$, the product of $g$ over $s$ is equal to the function that maps each $a \in \alpha$ to the product over $s$ of the evaluations $g(c)(a)$. In other words, \[ \prod_{c \in s} g(c) = \left(a \mapsto \prod_{c \in s} g(c)(a)\right). \]

Fintype.prod_apply theorem

 {α : Type*} {β : α → Type*} {γ : Type*} [Fintype γ] [∀ a, CommMonoid (β a)] (a : α) (g : γ → ∀ a, β a) :
  (∏ c, g c) a = ∏ c, g c a

Full source

@[to_additive]
theorem Fintype.prod_apply {α : Type*} {β : α → Type*} {γ : Type*} [Fintype γ]
    [∀ a, CommMonoid (β a)] (a : α) (g : γ → ∀ a, β a) : (∏ c, g c) a = ∏ c, g c a :=
  Finset.prod_apply a Finset.univ g

Evaluation of Finite Product over Entire Type in Function Space

Informal description

Let $\alpha$ be a type, and for each $a \in \alpha$, let $\beta(a)$ be a commutative monoid. Let $\gamma$ be a finite type. For any fixed $a \in \alpha$ and any function $g \colon \gamma \to \prod_{a \in \alpha} \beta(a)$, the evaluation at $a$ of the product of $g$ over all elements of $\gamma$ is equal to the product over all elements of $\gamma$ of the evaluations $g(c)(a)$. In other words, \[ \left(\prod_{c \in \gamma} g(c)\right)(a) = \prod_{c \in \gamma} g(c)(a). \]

prod_mk_prod theorem

 {α β γ : Type*} [CommMonoid α] [CommMonoid β] (s : Finset γ) (f : γ → α) (g : γ → β) :
  (∏ x ∈ s, f x, ∏ x ∈ s, g x) = ∏ x ∈ s, (f x, g x)

Full source

@[to_additive prod_mk_sum]
theorem prod_mk_prod {α β γ : Type*} [CommMonoid α] [CommMonoid β] (s : Finset γ) (f : γ → α)
    (g : γ → β) : (∏ x ∈ s, f x, ∏ x ∈ s, g x) = ∏ x ∈ s, (f x, g x) :=
  haveI := Classical.decEq γ
  Finset.induction_on s rfl (by simp +contextual [Prod.ext_iff])

Product of Pairs Equals Pair of Products in Commutative Monoids

Informal description

Let $\alpha$ and $\beta$ be commutative monoids, $\gamma$ a type, and $s$ a finite subset of $\gamma$. For any functions $f \colon \gamma \to \alpha$ and $g \colon \gamma \to \beta$, the pair of products $(\prod_{x \in s} f(x), \prod_{x \in s} g(x))$ is equal to the product of pairs $\prod_{x \in s} (f(x), g(x))$.

pi_eq_sum_univ theorem

 {ι : Type*} [Fintype ι] [DecidableEq ι] {R : Type*} [NonAssocSemiring R] (x : ι → R) :
  x = ∑ i, (x i) • fun j => if i = j then (1 : R) else 0

Full source

/-- decomposing `x : ι → R` as a sum along the canonical basis -/
theorem pi_eq_sum_univ {ι : Type*} [Fintype ι] [DecidableEq ι] {R : Type*} [NonAssocSemiring R]
    (x : ι → R) : x = ∑ i, (x i) • fun j => if i = j then (1 : R) else 0 := by
  ext
  simp

Decomposition of a Function into a Linear Combination of Indicator Functions

Informal description

Let $\iota$ be a finite type with decidable equality and $R$ be a non-associative semiring. For any function $x : \iota \to R$, we have the decomposition: \[ x = \sum_{i \in \iota} x(i) \cdot \mathbf{1}_{\{i\}} \] where $\mathbf{1}_{\{i\}}$ is the indicator function defined by $\mathbf{1}_{\{i\}}(j) = 1$ if $i = j$ and $0$ otherwise.

prod_indicator_apply theorem

 (s : Finset ι) (f : ι → Set κ) (g : ι → κ → α) (j : κ) :
  ∏ i ∈ s, (f i).indicator (g i) j = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) j

Full source

lemma prod_indicator_apply (s : Finset ι) (f : ι → Set κ) (g : ι → κ → α) (j : κ) :
    ∏ i ∈ s, (f i).indicator (g i) j = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) j := by
  rw [Set.indicator]
  split_ifs with hj
  · rw [Finset.prod_apply]
    congr! 1 with i hi
    simp only [Finset.inf_set_eq_iInter, Set.mem_iInter] at hj
    exact Set.indicator_of_mem (hj _ hi) _
  · obtain ⟨i, hi, hj⟩ := by simpa using hj
    exact Finset.prod_eq_zero hi <| Set.indicator_of_not_mem hj _

Product of Indicator Functions Equals Indicator of Intersection Applied to Product

Informal description

Let $s$ be a finite set of indices of type $\iota$, $f \colon \iota \to \text{Set } \kappa$ a family of sets, and $g \colon \iota \to \kappa \to \alpha$ a family of functions. For any fixed element $j \in \kappa$, the product over $s$ of the indicator functions $(f(i)).\text{indicator}(g(i))$ evaluated at $j$ is equal to the indicator function of the intersection $\bigcap_{x \in s} f(x)$ evaluated at the product $\prod_{i \in s} g(i)(j)$. In mathematical notation: \[ \prod_{i \in s} \mathbf{1}_{f(i)}(g(i))(j) = \mathbf{1}_{\bigcap_{x \in s} f(x)}\left(\prod_{i \in s} g(i)\right)(j). \]

prod_indicator theorem

 (s : Finset ι) (f : ι → Set κ) (g : ι → κ → α) :
  ∏ i ∈ s, (f i).indicator (g i) = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i)

Full source

lemma prod_indicator (s : Finset ι) (f : ι → Set κ) (g : ι → κ → α) :
    ∏ i ∈ s, (f i).indicator (g i) = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) := by
  ext a; simpa using prod_indicator_apply ..

Product of Indicator Functions Equals Indicator of Intersection Applied to Product

Informal description

Let $s$ be a finite set of indices of type $\iota$, $f \colon \iota \to \text{Set } \kappa$ a family of sets, and $g \colon \iota \to \kappa \to \alpha$ a family of functions. The product over $s$ of the indicator functions $\mathbf{1}_{f(i)}(g(i))$ is equal to the indicator function of the intersection $\bigcap_{x \in s} f(x)$ applied to the product $\prod_{i \in s} g(i)$. In mathematical notation: \[ \prod_{i \in s} \mathbf{1}_{f(i)}(g(i)) = \mathbf{1}_{\bigcap_{x \in s} f(x)}\left(\prod_{i \in s} g(i)\right). \]

prod_indicator_const_apply theorem

 (s : Finset ι) (f : ι → Set κ) (g : κ → α) (j : κ) : ∏ i ∈ s, (f i).indicator g j = (⋂ x ∈ s, f x).indicator (g ^ #s) j

Full source

lemma prod_indicator_const_apply (s : Finset ι) (f : ι → Set κ) (g : κ → α) (j : κ) :
    ∏ i ∈ s, (f i).indicator g j = (⋂ x ∈ s, f x).indicator (g ^ #s) j := by
  simp [prod_indicator_apply]

Product of Constant Indicator Functions Equals Indicator of Intersection Applied to Power Function

Informal description

Let $s$ be a finite set of indices of type $\iota$, $f \colon \iota \to \text{Set } \kappa$ a family of sets, and $g \colon \kappa \to \alpha$ a function. For any fixed element $j \in \kappa$, the product over $s$ of the indicator functions $\mathbf{1}_{f(i)}(g)$ evaluated at $j$ is equal to the indicator function of the intersection $\bigcap_{x \in s} f(x)$ evaluated at $g(j)^{|s|}$. In mathematical notation: \[ \prod_{i \in s} \mathbf{1}_{f(i)}(g)(j) = \mathbf{1}_{\bigcap_{x \in s} f(x)}(g^{|s|})(j). \]

prod_indicator_const theorem

 (s : Finset ι) (f : ι → Set κ) (g : κ → α) : ∏ i ∈ s, (f i).indicator g = (⋂ x ∈ s, f x).indicator (g ^ #s)

Full source

lemma prod_indicator_const (s : Finset ι) (f : ι → Set κ) (g : κ → α) :
    ∏ i ∈ s, (f i).indicator g = (⋂ x ∈ s, f x).indicator (g ^ #s) := by simp [prod_indicator]

Product of Constant Indicator Functions Equals Indicator of Intersection Applied to Power Function

Informal description

Let $s$ be a finite set of indices of type $\iota$, $f \colon \iota \to \text{Set } \kappa$ a family of sets, and $g \colon \kappa \to \alpha$ a function. The product over $s$ of the indicator functions $\mathbf{1}_{f(i)}(g)$ is equal to the indicator function of the intersection $\bigcap_{x \in s} f(x)$ applied to the $|s|$-th power of $g$, where $|s|$ denotes the cardinality of $s$. In mathematical notation: \[ \prod_{i \in s} \mathbf{1}_{f(i)}(g) = \mathbf{1}_{\bigcap_{x \in s} f(x)}(g^{|s|}). \]

Finset.univ_prod_mulSingle theorem

[Fintype I] (f : ∀ i, Z i) : (∏ i, Pi.mulSingle i (f i)) = f

Full source

@[to_additive]
theorem Finset.univ_prod_mulSingle [Fintype I] (f : ∀ i, Z i) :
    (∏ i, Pi.mulSingle i (f i)) = f := by
  ext a
  simp

Product of Multiplicative Single Functions Equals Original Function

Informal description

Let $I$ be a finite type and for each $i \in I$, let $Z_i$ be a commutative monoid. For any function $f \colon \prod_{i \in I} Z_i$, the product over all $i \in I$ of the multiplicative single functions $\text{mulSingle}_i(f(i))$ equals $f$ itself. That is, \[ \prod_{i \in I} \text{mulSingle}_i(f(i)) = f, \] where $\text{mulSingle}_i(x)$ is the function that takes value $x$ at $i$ and $1$ (the multiplicative identity) elsewhere.

MonoidHom.functions_ext theorem

 [Finite I] (G : Type*) [CommMonoid G] (g h : (∀ i, Z i) →* G)
  (H : ∀ i x, g (Pi.mulSingle i x) = h (Pi.mulSingle i x)) : g = h

Full source

@[to_additive]
theorem MonoidHom.functions_ext [Finite I] (G : Type*) [CommMonoid G] (g h : (∀ i, Z i) →* G)
    (H : ∀ i x, g (Pi.mulSingle i x) = h (Pi.mulSingle i x)) : g = h := by
  cases nonempty_fintype I
  ext k
  rw [← Finset.univ_prod_mulSingle k, map_prod, map_prod]
  simp only [H]

Extensionality of Monoid Homomorphisms via Multiplicative Single Functions

Informal description

Let $I$ be a finite index set, $G$ a commutative monoid, and $g, h \colon \prod_{i \in I} Z_i \to G$ monoid homomorphisms. If for every $i \in I$ and every $x \in Z_i$, we have $g(\text{mulSingle}_i(x)) = h(\text{mulSingle}_i(x))$, where $\text{mulSingle}_i(x)$ is the function that equals $x$ at $i$ and $1$ elsewhere, then $g = h$.

MonoidHom.functions_ext' theorem

 [Finite I] (M : Type*) [CommMonoid M] (g h : (∀ i, Z i) →* M)
  (H : ∀ i, g.comp (MonoidHom.mulSingle Z i) = h.comp (MonoidHom.mulSingle Z i)) : g = h

Full source

/-- This is used as the ext lemma instead of `MonoidHom.functions_ext` for reasons explained in
note [partially-applied ext lemmas]. -/
@[to_additive (attr := ext)
      "\nThis is used as the ext lemma instead of `AddMonoidHom.functions_ext` for reasons
      explained in note [partially-applied ext lemmas]."]
theorem MonoidHom.functions_ext' [Finite I] (M : Type*) [CommMonoid M] (g h : (∀ i, Z i) →* M)
    (H : ∀ i, g.comp (MonoidHom.mulSingle Z i) = h.comp (MonoidHom.mulSingle Z i)) : g = h :=
  g.functions_ext M h fun i => DFunLike.congr_fun (H i)

Extensionality of Monoid Homomorphisms via Composition with Multiplicative Single Functions

Informal description

Let $I$ be a finite index set, $M$ a commutative monoid, and $g, h \colon \prod_{i \in I} Z_i \to M$ monoid homomorphisms. If for every $i \in I$, the compositions $g \circ \text{mulSingle}_i$ and $h \circ \text{mulSingle}_i$ are equal, where $\text{mulSingle}_i \colon Z_i \to \prod_{i \in I} Z_i$ is the homomorphism that maps $x \in Z_i$ to the function that is $x$ at index $i$ and the identity element elsewhere, then $g = h$.

RingHom.functions_ext theorem

 [Finite I] (G : Type*) [NonAssocSemiring G] (g h : (∀ i, f i) →+* G)
  (H : ∀ (i : I) (x : f i), g (single i x) = h (single i x)) : g = h

Full source

@[ext]
theorem RingHom.functions_ext [Finite I] (G : Type*) [NonAssocSemiring G] (g h : (∀ i, f i) →+* G)
    (H : ∀ (i : I) (x : f i), g (single i x) = h (single i x)) : g = h :=
  RingHom.coe_addMonoidHom_injective <|
    @AddMonoidHom.functions_ext I _ f _ _ G _ (g : (∀ i, f i) →+ G) h H

Extensionality of Ring Homomorphisms via Single Functions

Informal description

Let $I$ be a finite index set, $G$ a non-associative semiring, and $g, h \colon \prod_{i \in I} f(i) \to G$ ring homomorphisms. If for every $i \in I$ and every $x \in f(i)$, we have $g(\text{single}_i(x)) = h(\text{single}_i(x))$, where $\text{single}_i(x)$ is the function that equals $x$ at $i$ and $0$ elsewhere, then $g = h$.

Prod.fst_prod theorem

: (∏ c ∈ s, f c).1 = ∏ c ∈ s, (f c).1

Full source

@[to_additive]
theorem fst_prod : (∏ c ∈ s, f c).1 = ∏ c ∈ s, (f c).1 :=
  map_prod (MonoidHom.fst α β) f s

First Projection of Product Equals Product of First Projections

Informal description

Let $M$ and $N$ be commutative monoids, and let $s$ be a finite set. For any function $f : s \to M \times N$, the first projection of the product $\prod_{c \in s} f(c)$ in $M \times N$ equals the product $\prod_{c \in s} (f(c))_1$ in $M$.

Prod.snd_prod theorem

: (∏ c ∈ s, f c).2 = ∏ c ∈ s, (f c).2

Full source

@[to_additive]
theorem snd_prod : (∏ c ∈ s, f c).2 = ∏ c ∈ s, (f c).2 :=
  map_prod (MonoidHom.snd α β) f s

Second Component of Product Equals Product of Second Components

Informal description

For any finite set $s$ and any function $f$ mapping elements of $s$ to pairs in a product of commutative monoids $M \times N$, the second component of the product $\prod_{c \in s} f(c)$ equals the product of the second components $\prod_{c \in s} (f(c))_2$.

Pi.monoidHomMulEquiv definition

 {ι : Type*} [Fintype ι] [DecidableEq ι] (M : ι → Type*) [(i : ι) → CommMonoid (M i)] (M' : Type*) [CommMonoid M'] :
  (((i : ι) → M i) →* M') ≃* ((i : ι) → (M i →* M'))

Full source

/-- The canonical isomorphism between the monoid of homomorphisms from a finite product of
commutative monoids to another commutative monoid and the product of the homomorphism monoids. -/
@[to_additive "The canonical isomorphism between the additive monoid of homomorphisms from
a finite product of additive commutative monoids to another additive commutative monoid and
the product of the homomorphism monoids."]
def Pi.monoidHomMulEquiv {ι : Type*} [Fintype ι] [DecidableEq ι] (M : ι → Type*)
    [(i : ι) → CommMonoid (M i)] (M' : Type*) [CommMonoid M'] :
    (((i : ι) → M i) →* M') ≃* ((i : ι) → (M i →* M')) where
  toFun φ i := φ.comp <| MonoidHom.mulSingle M i
  invFun φ := ∏ (i : ι), (φ i).comp (Pi.evalMonoidHom M i)
  left_inv φ := by
    ext
    simp only [MonoidHom.finset_prod_apply, MonoidHom.coe_comp, Function.comp_apply,
      evalMonoidHom_apply, MonoidHom.mulSingle_apply, ← map_prod]
    refine congrArg _ <| funext fun _ ↦ ?_
    rw [Fintype.prod_apply]
    exact Fintype.prod_pi_mulSingle ..
  right_inv φ := by
    ext i m
    simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.mulSingle_apply,
      MonoidHom.finset_prod_apply, evalMonoidHom_apply, ]
    let φ' i : M i → M' := ⇑(φ i)
    conv =>
      enter [1, 2, j]
      rw [show φ j = φ' j from rfl, Pi.apply_mulSingle φ' (fun i ↦ map_one (φ i))]
    rw [show φ' i = φ i from rfl]
    exact Fintype.prod_pi_mulSingle' ..
  map_mul' φ ψ := by
    ext
    simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.mulSingle_apply,
      MonoidHom.mul_apply, mul_apply]

Multiplicative Equivalence Between Homomorphisms from a Finite Product and Product of Homomorphism Monoids

Informal description

Given a finite index type $\iota$ and a family of commutative monoids $(M_i)_{i \in \iota}$, there is a multiplicative equivalence between the monoid of homomorphisms from the product monoid $\prod_{i \in \iota} M_i$ to a commutative monoid $M'$ and the product monoid $\prod_{i \in \iota} (M_i \to^* M')$ of homomorphism monoids. Explicitly: - The forward map takes a homomorphism $\varphi \colon \prod_{i \in \iota} M_i \to^* M'$ and returns the family of homomorphisms $(\varphi \circ \text{mulSingle}_i)_{i \in \iota}$, where $\text{mulSingle}_i \colon M_i \to^* \prod_{i \in \iota} M_i$ is the canonical inclusion. - The inverse map takes a family of homomorphisms $(\varphi_i \colon M_i \to^* M')_{i \in \iota}$ and constructs the homomorphism $\prod_{i \in \iota} (\varphi_i \circ \text{eval}_i)$, where $\text{eval}_i \colon \prod_{i \in \iota} M_i \to^* M_i$ is the evaluation map at index $i$. This equivalence preserves the multiplicative structure, i.e., the pointwise product of homomorphisms corresponds to the product in the homomorphism monoid.

Pi.single_induction theorem

 [AddCommMonoid M] (p : (ι → M) → Prop) (f : ι → M) (zero : p 0) (add : ∀ f g, p f → p g → p (f + g))
  (single : ∀ i m, p (Pi.single i m)) : p f

Full source

lemma Pi.single_induction [AddCommMonoid M] (p : (ι → M) → Prop) (f : ι → M)
    (zero : p 0) (add : ∀ f g, p f → p g → p (f + g))
    (single : ∀ i m, p (Pi.single i m)) : p f := by
  cases nonempty_fintype ι
  rw [← Finset.univ_sum_single f]
  exact Finset.sum_induction _ _ add zero (by simp [single])

Induction Principle for Functions via Single-Element Functions in Additive Commutative Monoids

Informal description

Let $M$ be an additive commutative monoid and $\iota$ be a finite type. For any predicate $p$ on functions $\iota \to M$, if $p$ holds for the zero function, is preserved under addition (i.e., $p(f)$ and $p(g)$ imply $p(f + g)$), and holds for all single-element functions $\mathrm{single}_i(m)$ (where $\mathrm{single}_i(m)$ is the function that is $m$ at $i$ and zero elsewhere), then $p$ holds for all functions $f : \iota \to M$.

Pi.mulSingle_induction theorem

 [CommMonoid M] (p : (ι → M) → Prop) (f : ι → M) (one : p 1) (mul : ∀ f g, p f → p g → p (f * g))
  (mulSingle : ∀ i m, p (Pi.mulSingle i m)) : p f

Full source

@[to_additive existing (attr := elab_as_elim)]
lemma Pi.mulSingle_induction [CommMonoid M] (p : (ι → M) → Prop) (f : ι → M)
    (one : p 1) (mul : ∀ f g, p f → p g → p (f * g))
    (mulSingle : ∀ i m, p (Pi.mulSingle i m)) : p f := by
  cases nonempty_fintype ι
  rw [← Finset.univ_prod_mulSingle f]
  exact Finset.prod_induction _ _ mul one (by simp [mulSingle])

Induction Principle for Multiplicative Single Functions in Commutative Monoids

Informal description

Let $M$ be a commutative monoid and $\iota$ be an index type. For any predicate $p$ on functions $\iota \to M$ and any function $f \colon \iota \to M$, if the following conditions hold: 1. $p$ holds for the constant function $1$ (the multiplicative identity), 2. $p$ is preserved under pointwise multiplication, i.e., for any $f, g \colon \iota \to M$, if $p(f)$ and $p(g)$ hold, then $p(f \cdot g)$ holds, 3. $p$ holds for all multiplicative single functions, i.e., for any $i \in \iota$ and $m \in M$, $p(\text{mulSingle}_i(m))$ holds, where $\text{mulSingle}_i(m)$ is the function that takes value $m$ at $i$ and $1$ elsewhere, then $p(f)$ holds.