Theorems · Theorem · group theory

Finset.noncommProd_congr

∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] {s₁ s₂ : Finset α} {f g : α → β} (h₁ : s₁ = s₂)
  (h₂ : ∀ x ∈ s₂, f x = g x) (comm : (↑s₁).Pairwise (Function.onFun Commute f)),
  s₁.noncommProd f comm = s₂.noncommProd g ⋯

Defined in

Mathlib.Data.Finset.NoncommProd

Cited by

13 results in Mathlib

Foundations

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

Assumes

Monoid