Mathlib Map

Theorems · Definition · number theory

Finset.mulDysonETransform

{α : Type u_1} → [DecidableEq α] → [CommGroup α] → α → Finset α × Finset α → Finset α × Finset α

The Dyson e-transform. Turns (s, t) into (s ∪ e • t, t ∩ e⁻¹ • s). This reduces the product of the two sets.

Defined in
Mathlib.Combinatorics.Additive.ETransform
Cited by
6 results in Mathlib
Foundations
Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
DecidableEqCommGroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Finset.mulDysonETransform_fst · cited by 0Finset.mulDysonETransform…Finset.mulDysonETransform_idem · cited by 0Finset.mulDysonETransform…Finset.mulDysonETransform_snd · cited by 0Finset.mulDysonETransform…Finset.mulDysonETransform.card · cited by 0mulDysonETransform.cardFinset.mulDysonETransform.smul_finset_snd_subset_fst · cited by 0mulDysonETransform.smul_f…Finset.mulDysonETransform.subset · cited by 0mulDysonETransform.subsetFinset · cited by 13712FinsetCommGroup · cited by 990CommGroupFinset.mulDysonETransformCITED BYCITES

Cites2

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

  • Finsetstatement and proof · cited by 13,712
  • CommGroupstatement and proof · cited by 990

Cited by6

Results whose statement or proof uses this declaration.