Theorems · Theorem · group theory

Finset.mul_noncommProd_erase

∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] [inst_1 : DecidableEq α] (s : Finset α) {a : α},
  a ∈ s →
    ∀ (f : α → β) (comm : (↑s).Pairwise (Function.onFun Commute f))
      (comm' : optParam (∀ x ∈ ↑(s.erase a), ∀ x_1 ∈ ↑(s.erase a), x ≠ x_1 → Function.onFun Commute f x x_1) ⋯),
      f a * (s.erase a).noncommProd f comm' = s.noncommProd f comm

Defined in

Mathlib.Data.Finset.NoncommProd

Cited by

0 results in Mathlib

Foundations

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

Assumes

MonoidDecidableEq