# Multiplication antidiagonal #

def Set.addAntidiagonal {α : Type u_1} [Add α] (s : Set α) (t : Set α) (a : α) :
Set (α × α)

Set.addAntidiagonal s t a is the set of all pairs of an element in s and an element in t that add to a.

Equations
Instances For
def Set.mulAntidiagonal {α : Type u_1} [Mul α] (s : Set α) (t : Set α) (a : α) :
Set (α × α)

Set.mulAntidiagonal s t a is the set of all pairs of an element in s and an element in t that multiply to a.

Equations
Instances For
@[simp]
theorem Set.mem_addAntidiagonal {α : Type u_1} [Add α] {s : Set α} {t : Set α} {a : α} {x : α × α} :
x s.addAntidiagonal t a x.1 s x.2 t x.1 + x.2 = a
@[simp]
theorem Set.mem_mulAntidiagonal {α : Type u_1} [Mul α] {s : Set α} {t : Set α} {a : α} {x : α × α} :
x s.mulAntidiagonal t a x.1 s x.2 t x.1 * x.2 = a
theorem Set.addAntidiagonal_mono_left {α : Type u_1} [Add α] {s₁ : Set α} {s₂ : Set α} {t : Set α} {a : α} (h : s₁ s₂) :
theorem Set.mulAntidiagonal_mono_left {α : Type u_1} [Mul α] {s₁ : Set α} {s₂ : Set α} {t : Set α} {a : α} (h : s₁ s₂) :
s₁.mulAntidiagonal t a s₂.mulAntidiagonal t a
theorem Set.addAntidiagonal_mono_right {α : Type u_1} [Add α] {s : Set α} {t₁ : Set α} {t₂ : Set α} {a : α} (h : t₁ t₂) :
theorem Set.mulAntidiagonal_mono_right {α : Type u_1} [Mul α] {s : Set α} {t₁ : Set α} {t₂ : Set α} {a : α} (h : t₁ t₂) :
s.mulAntidiagonal t₁ a s.mulAntidiagonal t₂ a
theorem Set.swap_mem_addAntidiagonal {α : Type u_1} [] {s : Set α} {t : Set α} {a : α} {x : α × α} :
theorem Set.swap_mem_mulAntidiagonal {α : Type u_1} [] {s : Set α} {t : Set α} {a : α} {x : α × α} :
x.swap s.mulAntidiagonal t a x t.mulAntidiagonal s a
@[simp]
theorem Set.swap_mem_addAntidiagonal_aux {α : Type u_1} [] {s : Set α} {t : Set α} {a : α} {x : α × α} :
x.2 s x.1 t x.2 + x.1 = a x t.addAntidiagonal s a
@[simp]
theorem Set.swap_mem_mulAntidiagonal_aux {α : Type u_1} [] {s : Set α} {t : Set α} {a : α} {x : α × α} :
x.2 s x.1 t x.2 * x.1 = a x t.mulAntidiagonal s a
theorem Set.AddAntidiagonal.fst_eq_fst_iff_snd_eq_snd {α : Type u_1} {s : Set α} {t : Set α} {a : α} {x : (s.addAntidiagonal t a)} {y : (s.addAntidiagonal t a)} :
(x).1 = (y).1 (x).2 = (y).2
theorem Set.MulAntidiagonal.fst_eq_fst_iff_snd_eq_snd {α : Type u_1} [] {s : Set α} {t : Set α} {a : α} {x : (s.mulAntidiagonal t a)} {y : (s.mulAntidiagonal t a)} :
(x).1 = (y).1 (x).2 = (y).2
theorem Set.AddAntidiagonal.eq_of_fst_eq_fst {α : Type u_1} {s : Set α} {t : Set α} {a : α} {x : (s.addAntidiagonal t a)} {y : (s.addAntidiagonal t a)} (h : (x).1 = (y).1) :
x = y
theorem Set.MulAntidiagonal.eq_of_fst_eq_fst {α : Type u_1} [] {s : Set α} {t : Set α} {a : α} {x : (s.mulAntidiagonal t a)} {y : (s.mulAntidiagonal t a)} (h : (x).1 = (y).1) :
x = y
theorem Set.AddAntidiagonal.eq_of_snd_eq_snd {α : Type u_1} {s : Set α} {t : Set α} {a : α} {x : (s.addAntidiagonal t a)} {y : (s.addAntidiagonal t a)} (h : (x).2 = (y).2) :
x = y
theorem Set.MulAntidiagonal.eq_of_snd_eq_snd {α : Type u_1} [] {s : Set α} {t : Set α} {a : α} {x : (s.mulAntidiagonal t a)} {y : (s.mulAntidiagonal t a)} (h : (x).2 = (y).2) :
x = y
theorem Set.AddAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd {α : Type u_1} (s : Set α) (t : Set α) (a : α) {x : (s.addAntidiagonal t a)} {y : (s.addAntidiagonal t a)} (h₁ : (x).1 (y).1) (h₂ : (x).2 (y).2) :
x = y
theorem Set.MulAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd {α : Type u_1} (s : Set α) (t : Set α) (a : α) {x : (s.mulAntidiagonal t a)} {y : (s.mulAntidiagonal t a)} (h₁ : (x).1 (y).1) (h₂ : (x).2 (y).2) :
x = y
theorem Set.AddAntidiagonal.finite_of_isPWO {α : Type u_1} {s : Set α} {t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) (a : α) :
theorem Set.MulAntidiagonal.finite_of_isPWO {α : Type u_1} {s : Set α} {t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) (a : α) :
(s.mulAntidiagonal t a).Finite
theorem Set.AddAntidiagonal.finite_of_isWF {α : Type u_1} {s : Set α} {t : Set α} (hs : s.IsWF) (ht : t.IsWF) (a : α) :