Theorems · Theorem · combinatorics

Set.VAddAntidiagonal.fst_eq_fst_iff_snd_eq_snd

∀ {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [inst : VAdd G P] {x y : ↑(s.vaddAntidiagonal t a)}
  [IsCancelVAdd G P], (↑x).1 = (↑y).1 ↔ (↑x).2 = (↑y).2

Defined in

Mathlib.Data.Set.SMulAntidiagonal

Cited by

1 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

VAddIsCancelVAdd