Documentation

Mathlib.Data.Set.MulAntidiagonal

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₂) :
      s₁.addAntidiagonal t a s₂.addAntidiagonal t a
      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₂) :
      s.addAntidiagonal t₁ a s.addAntidiagonal t₂ a
      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} [AddCommSemigroup α] {s : Set α} {t : Set α} {a : α} {x : α × α} :
      x.swap s.addAntidiagonal t a x t.addAntidiagonal s a
      theorem Set.swap_mem_mulAntidiagonal {α : Type u_1} [CommSemigroup α] {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} [AddCommSemigroup α] {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} [CommSemigroup α] {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} [AddCancelCommMonoid α] {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} [CancelCommMonoid α] {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} [AddCancelCommMonoid α] {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} [CancelCommMonoid α] {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} [AddCancelCommMonoid α] {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} [CancelCommMonoid α] {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} [AddCancelCommMonoid α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (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} [CancelCommMonoid α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] (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} [AddCancelCommMonoid α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {s : Set α} {t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) (a : α) :
      (s.addAntidiagonal t a).Finite
      theorem Set.MulAntidiagonal.finite_of_isPWO {α : Type u_1} [CancelCommMonoid α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {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} [AddCancelCommMonoid α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {s : Set α} {t : Set α} (hs : s.IsWF) (ht : t.IsWF) (a : α) :
      (s.addAntidiagonal t a).Finite
      theorem Set.MulAntidiagonal.finite_of_isWF {α : Type u_1} [CancelCommMonoid α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {s : Set α} {t : Set α} (hs : s.IsWF) (ht : t.IsWF) (a : α) :
      (s.mulAntidiagonal t a).Finite