Theorems · Definition · combinatorics
Set.vaddAntidiagonal
{G : Type u_1} → {P : Type u_2} → [VAdd G P] → Set G → Set P → P → Set (G × P)vaddAntidiagonal s t a is the set of all pairs of an element in s and an
element in t that vector-add to a.
- Defined in
- Mathlib.Data.Set.SMulAntidiagonal
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- VAdd
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.
- Setstatement and proof · cited by 53,352
- Set.ofPredproof · cited by 6,101
- HVAdd.hVAddproof · cited by 1,820
- VAddstatement and proof · cited by 616
Cited by20
Results whose statement or proof uses this declaration.
- Finset.VAddAntidiagonalstatement and proof · cited by 27
- Set.VAddAntidiagonal.finite_of_isPWOstatement and proof · cited by 16
- Finset.mem_vaddAntidiagonalstatement and proof · cited by 5
- Set.VAddAntidiagonal.finite_of_finitestatement and proof · cited by 5
- Finset.VAddAntidiagonal.congr_simpstatement and proof · cited by 4
- Finset.support_vaddAntidiagonal_subset_vaddstatement and proof · cited by 3
- Set.mem_vaddAntidiagonalstatement · cited by 2
- AddMonoidAlgebra.smul_eqstatement and proof · cited by 2
- Finset.vaddAntidiagonal_mono_leftstatement and proof · cited by 1
- Finset.vaddAntidiagonal_mono_rightstatement and proof · cited by 1
- Set.vaddAntidiagonal_mono_leftstatement and proof · cited by 1
- Set.vaddAntidiagonal_mono_rightstatement and proof · cited by 1