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.

source
theorem Set.IsPWO.mul {α : Type u_1} {s t : Set α} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] (hs : s.IsPWO) (ht : t.IsPWO) :
(s * t).IsPWO
source
theorem Set.IsPWO.add {α : Type u_1} {s t : Set α} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] (hs : s.IsPWO) (ht : t.IsPWO) :
(s + t).IsPWO
source
theorem Set.IsWF.mul {α : Type u_1} {s t : Set α} [CommMonoid α] [LinearOrder α] [IsOrderedCancelMonoid α] (hs : s.IsWF) (ht : t.IsWF) :
(s * t).IsWF
source
theorem Set.IsWF.add {α : Type u_1} {s t : Set α} [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] (hs : s.IsWF) (ht : t.IsWF) :
(s + t).IsWF
source
theorem Set.IsWF.min_mul {α : Type u_1} {s t : Set α} [CommMonoid α] [LinearOrder α] [IsOrderedCancelMonoid α] (hs : s.IsWF) (ht : t.IsWF) (hsn : s.Nonempty) (htn : t.Nonempty) :
⋯.min ⋯ = hs.min hsn * ht.min htn
source
theorem Set.IsWF.min_add {α : Type u_1} {s t : Set α} [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] (hs : s.IsWF) (ht : t.IsWF) (hsn : s.Nonempty) (htn : t.Nonempty) :
⋯.min ⋯ = hs.min hsn + ht.min htn
source
noncomputable def Finset.mulAntidiagonal {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s 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
Instances For
    source
    noncomputable def Finset.antidiagonal {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) (a : α) :
    Finset (α × α)

    Finset.antidiagonal 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
    Instances For
      source
      @[simp]
      theorem Finset.mem_mulAntidiagonal {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {x : α × α} :
      x ∈ mulAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 * x.2 = a
      source
      @[simp]
      theorem Finset.mem_antidiagonal {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {x : α × α} :
      x ∈ antidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 + x.2 = a
      source
      theorem Finset.mulAntidiagonal_mono_left {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {u : Set α} {hu : u.IsPWO} (h : u ⊆ s) :
      mulAntidiagonal hu ht a ⊆ mulAntidiagonal hs ht a
      source
      theorem Finset.antidiagonal_mono_left {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {u : Set α} {hu : u.IsPWO} (h : u ⊆ s) :
      antidiagonal hu ht a ⊆ antidiagonal hs ht a
      source
      theorem Finset.mulAntidiagonal_mono_right {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {u : Set α} {hu : u.IsPWO} (h : u ⊆ t) :
      mulAntidiagonal hs hu a ⊆ mulAntidiagonal hs ht a
      source
      theorem Finset.antidiagonal_mono_right {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {u : Set α} {hu : u.IsPWO} (h : u ⊆ t) :
      antidiagonal hs hu a ⊆ antidiagonal hs ht a
      source
      theorem Finset.swap_mem_mulAntidiagonal {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {x : α × α} :
      x.swap ∈ mulAntidiagonal hs ht a ↔ x ∈ mulAntidiagonal ht hs a
      source
      theorem Finset.swap_mem_antidiagonal {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {x : α × α} :
      x.swap ∈ antidiagonal hs ht a ↔ x ∈ antidiagonal ht hs a
      source
      theorem Finset.support_mulAntidiagonal_subset_mul {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} :
      {a : α | (mulAntidiagonal hs ht a).Nonempty} ⊆ s * t
      source
      theorem Finset.support_antidiagonal_subset_add {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} :
      {a : α | (antidiagonal hs ht a).Nonempty} ⊆ s + t
      source
      theorem Finset.isPWO_support_mulAntidiagonal {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} :
      {a : α | (mulAntidiagonal hs ht a).Nonempty}.IsPWO
      source
      theorem Finset.isPWO_support_antidiagonal {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} :
      {a : α | (antidiagonal hs ht a).Nonempty}.IsPWO
      source
      theorem Finset.mulAntidiagonal_min_mul_min {α : Type u_2} [CommMonoid α] [LinearOrder α] [IsOrderedCancelMonoid α] {s t : Set α} (hs : s.IsWF) (ht : t.IsWF) (hns : s.Nonempty) (hnt : t.Nonempty) :
      mulAntidiagonal ⋯ ⋯ (hs.min hns * ht.min hnt) = {(hs.min hns, ht.min hnt)}
      source
      theorem Finset.antidiagonal_min_add_min {α : Type u_2} [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] {s t : Set α} (hs : s.IsWF) (ht : t.IsWF) (hns : s.Nonempty) (hnt : t.Nonempty) :
      antidiagonal ⋯ ⋯ (hs.min hns + ht.min hnt) = {(hs.min hns, ht.min hnt)}
      source
      @[deprecated Finset.antidiagonal (since := "2026-06-08")]
      def Finset.addAntidiagonal {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) (a : α) :
      Finset (α × α)

      Alias of Finset.antidiagonal.

      Finset.antidiagonal 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
      Instances For
        source
        @[deprecated Finset.mem_antidiagonal (since := "2026-06-08")]
        theorem Finset.mem_addAntidiagonal {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {x : α × α} :
        x ∈ antidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 + x.2 = a

        Alias of Finset.mem_antidiagonal.

        source
        @[deprecated Finset.antidiagonal_mono_left (since := "2026-06-08")]
        theorem Finset.addAntidiagonal_mono_left {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {u : Set α} {hu : u.IsPWO} (h : u ⊆ s) :
        antidiagonal hu ht a ⊆ antidiagonal hs ht a

        Alias of Finset.antidiagonal_mono_left.

        source
        @[deprecated Finset.antidiagonal_mono_right (since := "2026-06-08")]
        theorem Finset.addAntidiagonal_mono_right {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {u : Set α} {hu : u.IsPWO} (h : u ⊆ t) :
        antidiagonal hs hu a ⊆ antidiagonal hs ht a

        Alias of Finset.antidiagonal_mono_right.

        source
        @[deprecated Finset.swap_mem_antidiagonal (since := "2026-06-08")]
        theorem Finset.swap_mem_addAntidiagonal {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {x : α × α} :
        x.swap ∈ antidiagonal hs ht a ↔ x ∈ antidiagonal ht hs a

        Alias of Finset.swap_mem_antidiagonal.

        source
        @[deprecated Finset.support_antidiagonal_subset_add (since := "2026-06-08")]
        theorem Finset.support_addAntidiagonal_subset_add {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} :
        {a : α | (antidiagonal hs ht a).Nonempty} ⊆ s + t

        Alias of Finset.support_antidiagonal_subset_add.

        source
        @[deprecated Finset.isPWO_support_antidiagonal (since := "2026-06-08")]
        theorem Finset.isPWO_support_addAntidiagonal {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} :
        {a : α | (antidiagonal hs ht a).Nonempty}.IsPWO

        Alias of Finset.isPWO_support_antidiagonal.

        source
        @[deprecated Finset.antidiagonal_min_add_min (since := "2026-06-08")]
        theorem Finset.addAntidiagonal_min_mul_min {α : Type u_2} [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] {s t : Set α} (hs : s.IsWF) (ht : t.IsWF) (hns : s.Nonempty) (hnt : t.Nonempty) :
        antidiagonal ⋯ ⋯ (hs.min hns + ht.min hnt) = {(hs.min hns, ht.min hnt)}

        Alias of Finset.antidiagonal_min_add_min.