mathlib3 documentation

data.set.mul_antidiagonal

Multiplication antidiagonal #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

def set.mul_antidiagonal {α : Type u_1} [has_mul α] (s t : set α) (a : α) :
set × α)

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

Equations
def set.add_antidiagonal {α : Type u_1} [has_add α] (s t : set α) (a : α) :
set × α)

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

Equations
@[simp]
theorem set.mem_add_antidiagonal {α : Type u_1} [has_add α] {s t : set α} {a : α} {x : α × α} :
x s.add_antidiagonal t a x.fst s x.snd t x.fst + x.snd = a
@[simp]
theorem set.mem_mul_antidiagonal {α : Type u_1} [has_mul α] {s t : set α} {a : α} {x : α × α} :
x s.mul_antidiagonal t a x.fst s x.snd t x.fst * x.snd = a
theorem set.mul_antidiagonal_mono_left {α : Type u_1} [has_mul α] {s₁ s₂ t : set α} {a : α} (h : s₁ s₂) :
theorem set.add_antidiagonal_mono_left {α : Type u_1} [has_add α] {s₁ s₂ t : set α} {a : α} (h : s₁ s₂) :
theorem set.mul_antidiagonal_mono_right {α : Type u_1} [has_mul α] {s t₁ t₂ : set α} {a : α} (h : t₁ t₂) :
theorem set.add_antidiagonal_mono_right {α : Type u_1} [has_add α] {s t₁ t₂ : set α} {a : α} (h : t₁ t₂) :
@[simp]
theorem set.swap_mem_mul_antidiagonal {α : Type u_1} [comm_semigroup α] {s t : set α} {a : α} {x : α × α} :
@[simp]
theorem set.swap_mem_add_antidiagonal {α : Type u_1} [add_comm_semigroup α] {s t : set α} {a : α} {x : α × α} :
theorem set.mul_antidiagonal.fst_eq_fst_iff_snd_eq_snd {α : Type u_1} [cancel_comm_monoid α] {s t : set α} {a : α} {x y : (s.mul_antidiagonal t a)} :
theorem set.add_antidiagonal.eq_of_fst_eq_fst {α : Type u_1} [add_cancel_comm_monoid α] {s t : set α} {a : α} {x y : (s.add_antidiagonal t a)} (h : x.fst = y.fst) :
x = y
theorem set.mul_antidiagonal.eq_of_fst_eq_fst {α : Type u_1} [cancel_comm_monoid α] {s t : set α} {a : α} {x y : (s.mul_antidiagonal t a)} (h : x.fst = y.fst) :
x = y
theorem set.add_antidiagonal.eq_of_snd_eq_snd {α : Type u_1} [add_cancel_comm_monoid α] {s t : set α} {a : α} {x y : (s.add_antidiagonal t a)} (h : x.snd = y.snd) :
x = y
theorem set.mul_antidiagonal.eq_of_snd_eq_snd {α : Type u_1} [cancel_comm_monoid α] {s t : set α} {a : α} {x y : (s.mul_antidiagonal t a)} (h : x.snd = y.snd) :
x = y
theorem set.mul_antidiagonal.eq_of_fst_le_fst_of_snd_le_snd {α : Type u_1} [ordered_cancel_comm_monoid α] (s t : set α) (a : α) {x y : (s.mul_antidiagonal t a)} (h₁ : x.fst y.fst) (h₂ : x.snd y.snd) :
x = y
theorem set.add_antidiagonal.eq_of_fst_le_fst_of_snd_le_snd {α : Type u_1} [ordered_cancel_add_comm_monoid α] (s t : set α) (a : α) {x y : (s.add_antidiagonal t a)} (h₁ : x.fst y.fst) (h₂ : x.snd y.snd) :
x = y
theorem set.mul_antidiagonal.finite_of_is_pwo {α : Type u_1} [ordered_cancel_comm_monoid α] {s t : set α} (hs : s.is_pwo) (ht : t.is_pwo) (a : α) :
theorem set.add_antidiagonal.finite_of_is_pwo {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s t : set α} (hs : s.is_pwo) (ht : t.is_pwo) (a : α) :
theorem set.add_antidiagonal.finite_of_is_wf {α : Type u_1} [linear_ordered_cancel_add_comm_monoid α] {s t : set α} (hs : s.is_wf) (ht : t.is_wf) (a : α) :
theorem set.mul_antidiagonal.finite_of_is_wf {α : Type u_1} [linear_ordered_cancel_comm_monoid α] {s t : set α} (hs : s.is_wf) (ht : t.is_wf) (a : α) :