# Documentation

Mathlib.Data.Finset.MulAntidiagonal

# 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 : ) (ht : ) :
Set.IsPwo (s + t)
theorem Set.IsPwo.mul {α : Type u_1} {s : Set α} {t : Set α} (hs : ) (ht : ) :
Set.IsPwo (s * t)
theorem Set.IsWf.add {α : Type u_1} {s : Set α} {t : Set α} (hs : ) (ht : ) :
Set.IsWf (s + t)
theorem Set.IsWf.mul {α : Type u_1} {s : Set α} {t : Set α} (hs : ) (ht : ) :
Set.IsWf (s * t)
theorem Set.IsWf.min_add {α : Type u_1} {s : Set α} {t : Set α} (hs : ) (ht : ) (hsn : ) (htn : ) :
Set.IsWf.min (_ : Set.IsWf (s + t)) (_ : Set.Nonempty (s + t)) = Set.IsWf.min hs hsn + Set.IsWf.min ht htn
theorem Set.IsWf.min_mul {α : Type u_1} {s : Set α} {t : Set α} (hs : ) (ht : ) (hsn : ) (htn : ) :
Set.IsWf.min (_ : Set.IsWf (s * t)) (_ : Set.Nonempty (s * t)) = Set.IsWf.min hs hsn * Set.IsWf.min ht htn
noncomputable def Finset.addAntidiagonal {α : Type u_1} {s : Set α} {t : Set α} (hs : ) (ht : ) (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.

Instances For
noncomputable def Finset.mulAntidiagonal {α : Type u_1} {s : Set α} {t : Set α} (hs : ) (ht : ) (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.

Instances For
@[simp]
theorem Finset.mem_addAntidiagonal {α : Type u_1} {s : Set α} {t : Set α} {hs : } {ht : } {a : α} {x : α × α} :
x x.fst s x.snd t x.fst + x.snd = a
@[simp]
theorem Finset.mem_mulAntidiagonal {α : Type u_1} {s : Set α} {t : Set α} {hs : } {ht : } {a : α} {x : α × α} :
x x.fst s x.snd t x.fst * x.snd = a
theorem Finset.addAntidiagonal_mono_left {α : Type u_1} {s : Set α} {t : Set α} {hs : } {ht : } {a : α} {u : Set α} {hu : } (h : u s) :
theorem Finset.mulAntidiagonal_mono_left {α : Type u_1} {s : Set α} {t : Set α} {hs : } {ht : } {a : α} {u : Set α} {hu : } (h : u s) :
theorem Finset.addAntidiagonal_mono_right {α : Type u_1} {s : Set α} {t : Set α} {hs : } {ht : } {a : α} {u : Set α} {hu : } (h : u t) :
theorem Finset.mulAntidiagonal_mono_right {α : Type u_1} {s : Set α} {t : Set α} {hs : } {ht : } {a : α} {u : Set α} {hu : } (h : u t) :
theorem Finset.swap_mem_addAntidiagonal {α : Type u_1} {s : Set α} {t : Set α} {hs : } {ht : } {a : α} {x : α × α} :
x
theorem Finset.swap_mem_mulAntidiagonal {α : Type u_1} {s : Set α} {t : Set α} {hs : } {ht : } {a : α} {x : α × α} :
x
abbrev Finset.support_addAntidiagonal_subset_add.match_1 {α : Type u_1} {s : Set α} {t : Set α} {hs : } {ht : } (a : α) (motive : a {a | Finset.Nonempty ()}Prop) :
(x : a {a | Finset.Nonempty ()}) → ((b : α × α) → (hb : b ) → motive (_ : x, x )) → motive x
Instances For
theorem Finset.support_addAntidiagonal_subset_add {α : Type u_1} {s : Set α} {t : Set α} {hs : } {ht : } :
{a | Finset.Nonempty ()} s + t
theorem Finset.support_mulAntidiagonal_subset_mul {α : Type u_1} {s : Set α} {t : Set α} {hs : } {ht : } :
{a | Finset.Nonempty ()} s * t
theorem Finset.isPwo_support_addAntidiagonal {α : Type u_1} {s : Set α} {t : Set α} {hs : } {ht : } :
theorem Finset.isPwo_support_mulAntidiagonal {α : Type u_1} {s : Set α} {t : Set α} {hs : } {ht : } :
theorem Finset.addAntidiagonal_min_add_min {α : Type u_2} {s : Set α} {t : Set α} (hs : ) (ht : ) (hns : ) (hnt : ) :
Finset.addAntidiagonal (_ : ) (_ : ) (Set.IsWf.min hs hns + Set.IsWf.min ht hnt) = {(Set.IsWf.min hs hns, Set.IsWf.min ht hnt)}
theorem Finset.mulAntidiagonal_min_mul_min {α : Type u_2} {s : Set α} {t : Set α} (hs : ) (ht : ) (hns : ) (hnt : ) :
Finset.mulAntidiagonal (_ : ) (_ : ) (Set.IsWf.min hs hns * Set.IsWf.min ht hnt) = {(Set.IsWf.min hs hns, Set.IsWf.min ht hnt)}