Theorems · Definition · combinatorics

Finset.VAddAntidiagonal

{G : Type u_1} →
  {P : Type u_2} →
    [inst : VAdd G P] → {s : Set G} → {t : Set P} → (a : P) → (s.vaddAntidiagonal t a).Finite → Finset (G × P)

Finset.VAddAntidiagonal hs ht a is the set of all pairs of an element in s and an element in t whose vector addition yields a, but its construction requires proofs that s and t are well-ordered.

Defined in

Mathlib.Data.Finset.SMulAntidiagonal

Cited by

27 results in Mathlib

Foundations

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

Assumes

VAdd