Theorems · Theorem · group theory

eqOn_fun_finsetProd

∀ {ι : Type u_8} {α : Type u_9} {β : Type u_10} [inst : CommMonoid α] {s : Set β} {f f' : ι → β → α},
  (∀ (i : ι), Set.EqOn (f i) (f' i) s) →
    ∀ (v : Finset ι), Set.EqOn (fun b => ∏ i ∈ v, f i b) (fun b => ∏ i ∈ v, f' i b) s

Defined in: Mathlib.Algebra.BigOperators.Pi
Cited by: 1 results in Mathlib
Foundations: Depth 18 from the axioms · uses propext, Quot.sound
Assumes: CommMonoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Finsetstatement and proof · cited by 13,712
Finset.prodstatement and proof · cited by 2,356
CommMonoidstatement and proof · cited by 2,264
Set.EqOnstatement and proof · cited by 603
Finset.prod_applyproof · cited by 70
eqOn_finsetProdproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

MultipliableLocallyUniformlyOn_congrproof · cited by 0