Theorems · Theorem · order theory

Finset.mem_mulAntidiagonal

∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {x : α × α},
  x ∈ Finset.mulAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 * x.2 = a

Defined in

Mathlib.Data.Finset.MulAntidiagonal

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidPartialOrderIsOrderedCancelMonoid