Theorems · Definition · number theory
Finset.addETransformRight
{α : Type u_1} → [DecidableEq α] → [AddGroup α] → α → Finset α × Finset α → Finset α × Finset αAn e-transform.
Turns (s, t) into (s ∪ s +ᵥ e, t ∩ -e +ᵥ t). This reduces the sum of the two sets.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEqAddGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- AddGroupstatement and proof · cited by 4,410
- HVAdd.hVAddproof · cited by 1,820
- AddOpposite.opproof · cited by 192
Cited by10
Results whose statement or proof uses this declaration.
- cauchy_davenport_minOrder_addproof · cited by 2
- Finset.AddETransform.cardstatement and proof · cited by 1
- Finset.addETransformLeft.cardstatement · cited by 1
- Finset.addETransformRight.cardstatement · cited by 1
- Finset.addETransformRight.fst_add_snd_subsetstatement · cited by 1
- Finset.addETransformLeft_negstatement · cited by 0
- Finset.addETransformRight_fststatement and proof · cited by 0
- Finset.addETransformRight_negstatement · cited by 0
- Finset.addETransformRight_sndstatement and proof · cited by 0
- Finset.addETransformRight_zerostatement · cited by 0