Theorems · Theorem · group theory

Finset.prod_mulIndicator_subset_of_eq_one

∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] [inst_1 : One α] (f : ι → α) (g : ι → α → β)
  {s t : Finset ι}, s ⊆ t → (∀ (a : ι), g a 1 = 1) → ∏ i ∈ t, g i ((↑s).mulIndicator f i) = ∏ i ∈ s, g i (f i)

Consider a product of g i (f i) over a finset. Suppose g is a function such as n ↦ (· ^ n), which maps a second argument of 1 to 1. Then if f is replaced by the corresponding multiplicative indicator function, the finset may be replaced by a possibly larger finset without changing the value of the product.

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Indicator

Cited by

1 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidOne