# Multiplication antidiagonal as a Finset. #

We construct the Finset of all pairs of an element in s and an element in t that multiply to a, given that s and t are well-ordered.

theorem Set.IsPWO.add {α : Type u_1} {s : Set α} {t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) :
(s + t).IsPWO
theorem Set.IsPWO.mul {α : Type u_1} {s : Set α} {t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) :
(s * t).IsPWO
theorem Set.IsWF.add {α : Type u_1} {s : Set α} {t : Set α} (hs : s.IsWF) (ht : t.IsWF) :
(s + t).IsWF
theorem Set.IsWF.mul {α : Type u_1} {s : Set α} {t : Set α} (hs : s.IsWF) (ht : t.IsWF) :
(s * t).IsWF
theorem Set.IsWF.min_add {α : Type u_1} {s : Set α} {t : Set α} (hs : s.IsWF) (ht : t.IsWF) (hsn : s.Nonempty) (htn : t.Nonempty) :
.min = hs.min hsn + ht.min htn
theorem Set.IsWF.min_mul {α : Type u_1} {s : Set α} {t : Set α} (hs : s.IsWF) (ht : t.IsWF) (hsn : s.Nonempty) (htn : t.Nonempty) :
.min = hs.min hsn * ht.min htn
noncomputable def Finset.addAntidiagonal {α : Type u_1} {s : Set α} {t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) (a : α) :
Finset (α × α)

Finset.addAntidiagonal hs ht a is the set of all pairs of an element in s and an element in t that add to a, but its construction requires proofs that s and t are well-ordered.

Equations
• = .toFinset
Instances For
noncomputable def Finset.mulAntidiagonal {α : Type u_1} {s : Set α} {t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) (a : α) :
Finset (α × α)

Finset.mulAntidiagonal hs ht a is the set of all pairs of an element in s and an element in t that multiply to a, but its construction requires proofs that s and t are well-ordered.

Equations
• = .toFinset
Instances For
@[simp]
theorem Finset.mem_addAntidiagonal {α : Type u_1} {s : Set α} {t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {x : α × α} :
x x.1 s x.2 t x.1 + x.2 = a
@[simp]
theorem Finset.mem_mulAntidiagonal {α : Type u_1} {s : Set α} {t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {x : α × α} :
x x.1 s x.2 t x.1 * x.2 = a
theorem Finset.addAntidiagonal_mono_left {α : Type u_1} {s : Set α} {t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {u : Set α} {hu : u.IsPWO} (h : u s) :
theorem Finset.mulAntidiagonal_mono_left {α : Type u_1} {s : Set α} {t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {u : Set α} {hu : u.IsPWO} (h : u s) :
theorem Finset.addAntidiagonal_mono_right {α : Type u_1} {s : Set α} {t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {u : Set α} {hu : u.IsPWO} (h : u t) :
theorem Finset.mulAntidiagonal_mono_right {α : Type u_1} {s : Set α} {t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {u : Set α} {hu : u.IsPWO} (h : u t) :
theorem Finset.swap_mem_addAntidiagonal {α : Type u_1} {s : Set α} {t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {x : α × α} :
x.swap x
theorem Finset.swap_mem_mulAntidiagonal {α : Type u_1} {s : Set α} {t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {x : α × α} :
x.swap x
theorem Finset.support_addAntidiagonal_subset_add {α : Type u_1} {s : Set α} {t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} :
{a : α | ().Nonempty} s + t
abbrev Finset.support_addAntidiagonal_subset_add.match_1 {α : Type u_1} {s : Set α} {t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} (a : α) (motive : a {a : α | ().Nonempty}Prop) :
∀ (x : a {a : α | ().Nonempty}), (∀ (b : α × α) (hb : b ), motive )motive x
Equations
• =
Instances For
theorem Finset.support_mulAntidiagonal_subset_mul {α : Type u_1} {s : Set α} {t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} :
{a : α | ().Nonempty} s * t
theorem Finset.isPWO_support_addAntidiagonal {α : Type u_1} {s : Set α} {t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} :
{a : α | ().Nonempty}.IsPWO
theorem Finset.isPWO_support_mulAntidiagonal {α : Type u_1} {s : Set α} {t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} :
{a : α | ().Nonempty}.IsPWO
theorem Finset.addAntidiagonal_min_add_min {α : Type u_2} {s : Set α} {t : Set α} (hs : s.IsWF) (ht : t.IsWF) (hns : s.Nonempty) (hnt : t.Nonempty) :
Finset.addAntidiagonal (hs.min hns + ht.min hnt) = {(hs.min hns, ht.min hnt)}
theorem Finset.mulAntidiagonal_min_mul_min {α : Type u_2} {s : Set α} {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)}