Theorems · Theorem · group theory

Finset.noncommProd_union_of_disjoint

∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] [inst_1 : DecidableEq α] {s t : Finset α},
  Disjoint s t →
    ∀ (f : α → β) (comm : (↑(s ∪ t)).Pairwise (Function.onFun Commute f)),
      (s ∪ t).noncommProd f comm = s.noncommProd f ⋯ * t.noncommProd f ⋯

The non-commutative version of Finset.prod_union

Defined in: Mathlib.Data.Finset.NoncommProd
Cited by: 1 results in Mathlib
Foundations: Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Monoid DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites24

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

Setstatement · cited by 53,352
Finsetstatement and proof · cited by 13,712
SetLike.coestatement and proof · cited by 8,199
Monoidstatement and proof · cited by 3,887
Multisetproof · cited by 2,627
Disjointstatement and proof · cited by 2,201
Multiset.mapproof · cited by 876
Commutestatement and proof · cited by 639
Function.onFunstatement and proof · cited by 570
Finset.valproof · cited by 438
Set.Pairwisestatement and proof · cited by 321
Multiset.ofListproof · cited by 290

Cited by1

Results whose statement or proof uses this declaration.

Equiv.Perm.Disjoint.cycleFactorsFinset_mul_eq_unionproof · cited by 2