Theorems · Theorem · order theory

Finset.mulAntidiagonal_min_mul_min

∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedCancelMonoid α] {s t : Set α}
  (hs : s.IsWF) (ht : t.IsWF) (hns : s.Nonempty) (hnt : t.Nonempty),
  Finset.mulAntidiagonal ⋯ ⋯ (hs.min hns * ht.min hnt) = {(hs.min hns, ht.min hnt)}

Defined in

Mathlib.Data.Finset.MulAntidiagonal

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommMonoidLinearOrderIsOrderedCancelMonoid