Theorems · Theorem · group theory

Finset.noncommProd_cons

∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] (s : Finset α) (a : α) (f : α → β) (ha : a ∉ s)
  (comm : (↑(Finset.cons a s ha)).Pairwise (Function.onFun Commute f)),
  (Finset.cons a s ha).noncommProd f comm = f a * s.noncommProd f ⋯

Defined in

Mathlib.Data.Finset.NoncommProd

Cited by

4 results in Mathlib

Foundations

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

Assumes

Monoid