Documentation

Mathlib.Data.Finset.Pointwise

Pointwise operations of finsets #

This file defines pointwise algebraic operations on finsets.

Main declarations #

For finsets s and t:

For α a semigroup/monoid, Finset α is a semigroup/monoid. As an unfortunate side effect, this means that n • s, where n : ℕ, is ambiguous between pointwise scaling and repeated pointwise addition; the former has (2 : ℕ) • {1, 2} = {2, 4}, while the latter has (2 : ℕ) • {1, 2} = {2, 3, 4}. See note [pointwise nat action].

Implementation notes #

We put all instances in the locale Pointwise, so that these instances are not available by default. Note that we do not mark them as reducible (as argued by note [reducible non-instances]) since we expect the locale to be open whenever the instances are actually used (and making the instances reducible changes the behavior of simp.

Tags #

finset multiplication, finset addition, pointwise addition, pointwise multiplication, pointwise subtraction

0/1 as finsets #

def Finset.zero {α : Type u_2} [Zero α] :

The finset 0 : Finset α is defined as {0} in locale Pointwise.

Equations
  • Finset.zero = { zero := {0} }
Instances For
    def Finset.one {α : Type u_2} [One α] :
    One (Finset α)

    The finset 1 : Finset α is defined as {1} in locale Pointwise.

    Equations
    • Finset.one = { one := {1} }
    Instances For
      @[simp]
      theorem Finset.mem_zero {α : Type u_2} [Zero α] {a : α} :
      a 0 a = 0
      @[simp]
      theorem Finset.mem_one {α : Type u_2} [One α] {a : α} :
      a 1 a = 1
      @[simp]
      theorem Finset.coe_zero {α : Type u_2} [Zero α] :
      0 = 0
      @[simp]
      theorem Finset.coe_one {α : Type u_2} [One α] :
      1 = 1
      @[simp]
      theorem Finset.zero_subset {α : Type u_2} [Zero α] {s : Finset α} :
      0 s 0 s
      @[simp]
      theorem Finset.one_subset {α : Type u_2} [One α] {s : Finset α} :
      1 s 1 s
      theorem Finset.singleton_zero {α : Type u_2} [Zero α] :
      {0} = 0
      theorem Finset.singleton_one {α : Type u_2} [One α] :
      {1} = 1
      theorem Finset.zero_mem_zero {α : Type u_2} [Zero α] :
      0 0
      theorem Finset.one_mem_one {α : Type u_2} [One α] :
      1 1
      @[simp]
      theorem Finset.map_zero {α : Type u_2} {β : Type u_3} [Zero α] {f : α β} :
      Finset.map f 0 = {f 0}
      @[simp]
      theorem Finset.map_one {α : Type u_2} {β : Type u_3} [One α] {f : α β} :
      Finset.map f 1 = {f 1}
      @[simp]
      theorem Finset.image_zero {α : Type u_2} {β : Type u_3} [Zero α] [DecidableEq β] {f : αβ} :
      Finset.image f 0 = {f 0}
      @[simp]
      theorem Finset.image_one {α : Type u_2} {β : Type u_3} [One α] [DecidableEq β] {f : αβ} :
      Finset.image f 1 = {f 1}
      theorem Finset.subset_zero_iff_eq {α : Type u_2} [Zero α] {s : Finset α} :
      s 0 s = s = 0
      theorem Finset.subset_one_iff_eq {α : Type u_2} [One α] {s : Finset α} :
      s 1 s = s = 1
      theorem Finset.Nonempty.subset_zero_iff {α : Type u_2} [Zero α] {s : Finset α} (h : Finset.Nonempty s) :
      s 0 s = 0
      theorem Finset.Nonempty.subset_one_iff {α : Type u_2} [One α] {s : Finset α} (h : Finset.Nonempty s) :
      s 1 s = 1
      @[simp]
      theorem Finset.card_zero {α : Type u_2} [Zero α] :
      @[simp]
      theorem Finset.card_one {α : Type u_2} [One α] :
      def Finset.singletonZeroHom {α : Type u_2} [Zero α] :
      ZeroHom α (Finset α)

      The singleton operation as a ZeroHom.

      Equations
      • Finset.singletonZeroHom = { toFun := singleton, map_zero' := (_ : {0} = 0) }
      Instances For
        def Finset.singletonOneHom {α : Type u_2} [One α] :
        OneHom α (Finset α)

        The singleton operation as a OneHom.

        Equations
        • Finset.singletonOneHom = { toFun := singleton, map_one' := (_ : {1} = 1) }
        Instances For
          @[simp]
          theorem Finset.coe_singletonZeroHom {α : Type u_2} [Zero α] :
          Finset.singletonZeroHom = singleton
          @[simp]
          theorem Finset.coe_singletonOneHom {α : Type u_2} [One α] :
          Finset.singletonOneHom = singleton
          @[simp]
          theorem Finset.singletonZeroHom_apply {α : Type u_2} [Zero α] (a : α) :
          Finset.singletonZeroHom a = {a}
          @[simp]
          theorem Finset.singletonOneHom_apply {α : Type u_2} [One α] (a : α) :
          Finset.singletonOneHom a = {a}
          theorem Finset.imageZeroHom.proof_1 {F : Type u_3} {α : Type u_2} {β : Type u_1} [Zero α] [DecidableEq β] [Zero β] [ZeroHomClass F α β] (f : F) :
          Finset.image (f) 0 = 0
          def Finset.imageZeroHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Zero α] [DecidableEq β] [Zero β] [ZeroHomClass F α β] (f : F) :

          Lift a ZeroHom to Finset via image

          Equations
          Instances For
            @[simp]
            theorem Finset.imageZeroHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [Zero α] [DecidableEq β] [Zero β] [ZeroHomClass F α β] (f : F) (s : Finset α) :
            @[simp]
            theorem Finset.imageOneHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [One α] [DecidableEq β] [One β] [OneHomClass F α β] (f : F) (s : Finset α) :
            def Finset.imageOneHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [One α] [DecidableEq β] [One β] [OneHomClass F α β] (f : F) :
            OneHom (Finset α) (Finset β)

            Lift a OneHom to Finset via image.

            Equations
            Instances For

              Finset negation/inversion #

              def Finset.neg {α : Type u_2} [DecidableEq α] [Neg α] :
              Neg (Finset α)

              The pointwise negation of finset -s is defined as {-x | x ∈ s} in locale Pointwise.

              Equations
              Instances For
                def Finset.inv {α : Type u_2} [DecidableEq α] [Inv α] :
                Inv (Finset α)

                The pointwise inversion of finset s⁻¹ is defined as {x⁻¹ | x ∈ s} in locale Pointwise.

                Equations
                Instances For
                  theorem Finset.neg_def {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} :
                  -s = Finset.image (fun x => -x) s
                  theorem Finset.inv_def {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} :
                  s⁻¹ = Finset.image (fun x => x⁻¹) s
                  theorem Finset.image_neg {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} :
                  Finset.image (fun x => -x) s = -s
                  theorem Finset.image_inv {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} :
                  Finset.image (fun x => x⁻¹) s = s⁻¹
                  theorem Finset.mem_neg {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} {x : α} :
                  x -s y, y s -y = x
                  theorem Finset.mem_inv {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} {x : α} :
                  x s⁻¹ y, y s y⁻¹ = x
                  theorem Finset.neg_mem_neg {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} {a : α} (ha : a s) :
                  -a -s
                  theorem Finset.inv_mem_inv {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} {a : α} (ha : a s) :
                  theorem Finset.card_neg_le {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} :
                  @[simp]
                  theorem Finset.neg_empty {α : Type u_2} [DecidableEq α] [Neg α] :
                  @[simp]
                  theorem Finset.inv_empty {α : Type u_2} [DecidableEq α] [Inv α] :
                  @[simp]
                  theorem Finset.Nonempty.inv {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} :

                  Alias of the reverse direction of Finset.inv_nonempty_iff.

                  Alias of the forward direction of Finset.inv_nonempty_iff.

                  theorem Finset.Nonempty.neg {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} :
                  theorem Finset.neg_subset_neg {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} {t : Finset α} (h : s t) :
                  -s -t
                  theorem Finset.inv_subset_inv {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} {t : Finset α} (h : s t) :
                  @[simp]
                  theorem Finset.neg_singleton {α : Type u_2} [DecidableEq α] [Neg α] (a : α) :
                  -{a} = {-a}
                  @[simp]
                  theorem Finset.inv_singleton {α : Type u_2} [DecidableEq α] [Inv α] (a : α) :
                  {a}⁻¹ = {a⁻¹}
                  @[simp]
                  theorem Finset.neg_insert {α : Type u_2} [DecidableEq α] [Neg α] (a : α) (s : Finset α) :
                  -insert a s = insert (-a) (-s)
                  @[simp]
                  theorem Finset.inv_insert {α : Type u_2} [DecidableEq α] [Inv α] (a : α) (s : Finset α) :
                  @[simp]
                  theorem Finset.coe_neg {α : Type u_2} [DecidableEq α] [InvolutiveNeg α] (s : Finset α) :
                  ↑(-s) = -s
                  @[simp]
                  theorem Finset.coe_inv {α : Type u_2} [DecidableEq α] [InvolutiveInv α] (s : Finset α) :
                  s⁻¹ = (s)⁻¹
                  @[simp]
                  theorem Finset.card_neg {α : Type u_2} [DecidableEq α] [InvolutiveNeg α] (s : Finset α) :
                  @[simp]
                  @[simp]
                  theorem Finset.preimage_neg {α : Type u_2} [DecidableEq α] [InvolutiveNeg α] (s : Finset α) :
                  Finset.preimage s Neg.neg (_ : Set.InjOn Neg.neg (Neg.neg ⁻¹' s)) = -s
                  @[simp]
                  theorem Finset.preimage_inv {α : Type u_2} [DecidableEq α] [InvolutiveInv α] (s : Finset α) :
                  Finset.preimage s Inv.inv (_ : Set.InjOn Inv.inv (Inv.inv ⁻¹' s)) = s⁻¹

                  Finset addition/multiplication #

                  def Finset.add {α : Type u_2} [DecidableEq α] [Add α] :
                  Add (Finset α)

                  The pointwise addition of finsets s + t is defined as {x + y | x ∈ s, y ∈ t} in locale Pointwise.

                  Equations
                  Instances For
                    def Finset.mul {α : Type u_2} [DecidableEq α] [Mul α] :
                    Mul (Finset α)

                    The pointwise multiplication of finsets s * t and t is defined as {x * y | x ∈ s, y ∈ t} in locale Pointwise.

                    Equations
                    Instances For
                      theorem Finset.add_def {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} :
                      s + t = Finset.image (fun p => p.fst + p.snd) (s ×ˢ t)
                      theorem Finset.mul_def {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} :
                      s * t = Finset.image (fun p => p.fst * p.snd) (s ×ˢ t)
                      theorem Finset.image_add_product {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} :
                      Finset.image (fun x => x.fst + x.snd) (s ×ˢ t) = s + t
                      theorem Finset.image_mul_product {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} :
                      Finset.image (fun x => x.fst * x.snd) (s ×ˢ t) = s * t
                      theorem Finset.mem_add {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} {x : α} :
                      x s + t y z, y s z t y + z = x
                      theorem Finset.mem_mul {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} {x : α} :
                      x s * t y z, y s z t y * z = x
                      @[simp]
                      theorem Finset.coe_add {α : Type u_2} [DecidableEq α] [Add α] (s : Finset α) (t : Finset α) :
                      ↑(s + t) = s + t
                      @[simp]
                      theorem Finset.coe_mul {α : Type u_2} [DecidableEq α] [Mul α] (s : Finset α) (t : Finset α) :
                      ↑(s * t) = s * t
                      theorem Finset.add_mem_add {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} {a : α} {b : α} :
                      a sb ta + b s + t
                      theorem Finset.mul_mem_mul {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} {a : α} {b : α} :
                      a sb ta * b s * t
                      theorem Finset.card_add_le {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} :
                      theorem Finset.card_mul_le {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} :
                      theorem Finset.card_add_iff {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} :
                      Finset.card (s + t) = Finset.card s * Finset.card t Set.InjOn (fun p => p.fst + p.snd) (s ×ˢ t)
                      theorem Finset.card_mul_iff {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} :
                      Finset.card (s * t) = Finset.card s * Finset.card t Set.InjOn (fun p => p.fst * p.snd) (s ×ˢ t)
                      @[simp]
                      theorem Finset.empty_add {α : Type u_2} [DecidableEq α] [Add α] (s : Finset α) :
                      @[simp]
                      theorem Finset.empty_mul {α : Type u_2} [DecidableEq α] [Mul α] (s : Finset α) :
                      @[simp]
                      theorem Finset.add_empty {α : Type u_2} [DecidableEq α] [Add α] (s : Finset α) :
                      @[simp]
                      theorem Finset.mul_empty {α : Type u_2} [DecidableEq α] [Mul α] (s : Finset α) :
                      @[simp]
                      theorem Finset.add_eq_empty {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} :
                      s + t = s = t =
                      @[simp]
                      theorem Finset.mul_eq_empty {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} :
                      s * t = s = t =
                      @[simp]
                      theorem Finset.add_nonempty {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} :
                      @[simp]
                      theorem Finset.mul_nonempty {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} :
                      theorem Finset.Nonempty.add {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} :
                      theorem Finset.Nonempty.mul {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} :
                      theorem Finset.Nonempty.of_add_left {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} :
                      theorem Finset.Nonempty.of_mul_left {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} :
                      theorem Finset.Nonempty.of_add_right {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} :
                      theorem Finset.Nonempty.of_mul_right {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} :
                      theorem Finset.add_singleton {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} (a : α) :
                      s + {a} = Finset.image (fun x => x + a) s
                      theorem Finset.mul_singleton {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} (a : α) :
                      s * {a} = Finset.image (fun x => x * a) s
                      theorem Finset.singleton_add {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} (a : α) :
                      {a} + s = Finset.image ((fun x x_1 => x + x_1) a) s
                      theorem Finset.singleton_mul {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} (a : α) :
                      {a} * s = Finset.image ((fun x x_1 => x * x_1) a) s
                      @[simp]
                      theorem Finset.singleton_add_singleton {α : Type u_2} [DecidableEq α] [Add α] (a : α) (b : α) :
                      {a} + {b} = {a + b}
                      @[simp]
                      theorem Finset.singleton_mul_singleton {α : Type u_2} [DecidableEq α] [Mul α] (a : α) (b : α) :
                      {a} * {b} = {a * b}
                      theorem Finset.add_subset_add {α : Type u_2} [DecidableEq α] [Add α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                      s₁ s₂t₁ t₂s₁ + t₁ s₂ + t₂
                      theorem Finset.mul_subset_mul {α : Type u_2} [DecidableEq α] [Mul α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                      s₁ s₂t₁ t₂s₁ * t₁ s₂ * t₂
                      theorem Finset.add_subset_add_left {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                      t₁ t₂s + t₁ s + t₂
                      theorem Finset.mul_subset_mul_left {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                      t₁ t₂s * t₁ s * t₂
                      theorem Finset.add_subset_add_right {α : Type u_2} [DecidableEq α] [Add α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
                      s₁ s₂s₁ + t s₂ + t
                      theorem Finset.mul_subset_mul_right {α : Type u_2} [DecidableEq α] [Mul α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
                      s₁ s₂s₁ * t s₂ * t
                      theorem Finset.add_subset_iff {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} {u : Finset α} :
                      s + t u ∀ (x : α), x s∀ (y : α), y tx + y u
                      theorem Finset.mul_subset_iff {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} {u : Finset α} :
                      s * t u ∀ (x : α), x s∀ (y : α), y tx * y u
                      theorem Finset.union_add {α : Type u_2} [DecidableEq α] [Add α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
                      s₁ s₂ + t = s₁ + t (s₂ + t)
                      theorem Finset.union_mul {α : Type u_2} [DecidableEq α] [Mul α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
                      (s₁ s₂) * t = s₁ * t s₂ * t
                      theorem Finset.add_union {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                      s + (t₁ t₂) = s + t₁ (s + t₂)
                      theorem Finset.mul_union {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                      s * (t₁ t₂) = s * t₁ s * t₂
                      theorem Finset.inter_add_subset {α : Type u_2} [DecidableEq α] [Add α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
                      s₁ s₂ + t (s₁ + t) (s₂ + t)
                      theorem Finset.inter_mul_subset {α : Type u_2} [DecidableEq α] [Mul α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
                      s₁ s₂ * t s₁ * t (s₂ * t)
                      theorem Finset.add_inter_subset {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                      s + t₁ t₂ (s + t₁) (s + t₂)
                      theorem Finset.mul_inter_subset {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                      s * (t₁ t₂) s * t₁ (s * t₂)
                      theorem Finset.inter_add_union_subset_union {α : Type u_2} [DecidableEq α] [Add α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                      s₁ s₂ + (t₁ t₂) s₁ + t₁ (s₂ + t₂)
                      theorem Finset.inter_mul_union_subset_union {α : Type u_2} [DecidableEq α] [Mul α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                      s₁ s₂ * (t₁ t₂) s₁ * t₁ s₂ * t₂
                      theorem Finset.union_add_inter_subset_union {α : Type u_2} [DecidableEq α] [Add α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                      s₁ s₂ + t₁ t₂ s₁ + t₁ (s₂ + t₂)
                      theorem Finset.union_mul_inter_subset_union {α : Type u_2} [DecidableEq α] [Mul α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                      (s₁ s₂) * (t₁ t₂) s₁ * t₁ s₂ * t₂
                      theorem Finset.subset_add {α : Type u_2} [DecidableEq α] [Add α] {u : Finset α} {s : Set α} {t : Set α} :
                      u s + ts' t', s' s t' t u s' + t'

                      If a finset u is contained in the sum of two sets s + t, we can find two finsets s', t' such that s' ⊆ s, t' ⊆ t and u ⊆ s' + t'.

                      theorem Finset.subset_mul {α : Type u_2} [DecidableEq α] [Mul α] {u : Finset α} {s : Set α} {t : Set α} :
                      u s * ts' t', s' s t' t u s' * t'

                      If a finset u is contained in the product of two sets s * t, we can find two finsets s', t' such that s' ⊆ s, t' ⊆ t and u ⊆ s' * t'.

                      theorem Finset.image_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Add α] [Add β] [AddHomClass F α β] (f : F) {s : Finset α} {t : Finset α} :
                      Finset.image (f) (s + t) = Finset.image (f) s + Finset.image (f) t
                      theorem Finset.image_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Mul α] [Mul β] [MulHomClass F α β] (f : F) {s : Finset α} {t : Finset α} :
                      Finset.image (f) (s * t) = Finset.image (f) s * Finset.image (f) t
                      def Finset.singletonAddHom {α : Type u_2} [DecidableEq α] [Add α] :
                      AddHom α (Finset α)

                      The singleton operation as an AddHom.

                      Equations
                      • Finset.singletonAddHom = { toFun := singleton, map_add' := (_ : ∀ (x x_1 : α), {x + x_1} = {x} + {x_1}) }
                      Instances For
                        theorem Finset.singletonAddHom.proof_1 {α : Type u_1} [DecidableEq α] [Add α] :
                        ∀ (x x_1 : α), {x + x_1} = {x} + {x_1}
                        def Finset.singletonMulHom {α : Type u_2} [DecidableEq α] [Mul α] :

                        The singleton operation as a MulHom.

                        Equations
                        • Finset.singletonMulHom = { toFun := singleton, map_mul' := (_ : ∀ (x x_1 : α), {x * x_1} = {x} * {x_1}) }
                        Instances For
                          @[simp]
                          theorem Finset.coe_singletonAddHom {α : Type u_2} [DecidableEq α] [Add α] :
                          Finset.singletonAddHom = singleton
                          @[simp]
                          theorem Finset.coe_singletonMulHom {α : Type u_2} [DecidableEq α] [Mul α] :
                          Finset.singletonMulHom = singleton
                          @[simp]
                          theorem Finset.singletonAddHom_apply {α : Type u_2} [DecidableEq α] [Add α] (a : α) :
                          Finset.singletonAddHom a = {a}
                          @[simp]
                          theorem Finset.singletonMulHom_apply {α : Type u_2} [DecidableEq α] [Mul α] (a : α) :
                          Finset.singletonMulHom a = {a}
                          theorem Finset.imageAddHom.proof_1 {F : Type u_3} {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [Add α] [Add β] [AddHomClass F α β] (f : F) :
                          ∀ (x x_1 : Finset α), Finset.image (f) (x + x_1) = Finset.image (f) x + Finset.image (f) x_1
                          def Finset.imageAddHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Add α] [Add β] [AddHomClass F α β] (f : F) :
                          AddHom (Finset α) (Finset β)

                          Lift an AddHom to Finset via image

                          Equations
                          Instances For
                            @[simp]
                            theorem Finset.imageAddHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Add α] [Add β] [AddHomClass F α β] (f : F) (s : Finset α) :
                            @[simp]
                            theorem Finset.imageMulHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Mul α] [Mul β] [MulHomClass F α β] (f : F) (s : Finset α) :
                            def Finset.imageMulHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Mul α] [Mul β] [MulHomClass F α β] (f : F) :

                            Lift a MulHom to Finset via image.

                            Equations
                            Instances For

                              Finset subtraction/division #

                              def Finset.sub {α : Type u_2} [DecidableEq α] [Sub α] :
                              Sub (Finset α)

                              The pointwise subtraction of finsets s - t is defined as {x - y | x ∈ s, y ∈ t} in locale Pointwise.

                              Equations
                              Instances For
                                def Finset.div {α : Type u_2} [DecidableEq α] [Div α] :
                                Div (Finset α)

                                The pointwise division of finsets s / t is defined as {x / y | x ∈ s, y ∈ t} in locale Pointwise.

                                Equations
                                Instances For
                                  theorem Finset.sub_def {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} :
                                  s - t = Finset.image (fun p => p.fst - p.snd) (s ×ˢ t)
                                  theorem Finset.div_def {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} :
                                  s / t = Finset.image (fun p => p.fst / p.snd) (s ×ˢ t)
                                  theorem Finset.add_image_prod {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} :
                                  Finset.image (fun x => x.fst - x.snd) (s ×ˢ t) = s - t
                                  theorem Finset.image_div_prod {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} :
                                  Finset.image (fun x => x.fst / x.snd) (s ×ˢ t) = s / t
                                  theorem Finset.mem_sub {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} {a : α} :
                                  a s - t b c, b s c t b - c = a
                                  theorem Finset.mem_div {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} {a : α} :
                                  a s / t b c, b s c t b / c = a
                                  @[simp]
                                  theorem Finset.coe_sub {α : Type u_2} [DecidableEq α] [Sub α] (s : Finset α) (t : Finset α) :
                                  ↑(s - t) = s - t
                                  @[simp]
                                  theorem Finset.coe_div {α : Type u_2} [DecidableEq α] [Div α] (s : Finset α) (t : Finset α) :
                                  ↑(s / t) = s / t
                                  theorem Finset.sub_mem_sub {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} {a : α} {b : α} :
                                  a sb ta - b s - t
                                  theorem Finset.div_mem_div {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} {a : α} {b : α} :
                                  a sb ta / b s / t
                                  theorem Finset.sub_card_le {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} :
                                  theorem Finset.div_card_le {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} :
                                  @[simp]
                                  theorem Finset.empty_sub {α : Type u_2} [DecidableEq α] [Sub α] (s : Finset α) :
                                  @[simp]
                                  theorem Finset.empty_div {α : Type u_2} [DecidableEq α] [Div α] (s : Finset α) :
                                  @[simp]
                                  theorem Finset.sub_empty {α : Type u_2} [DecidableEq α] [Sub α] (s : Finset α) :
                                  @[simp]
                                  theorem Finset.div_empty {α : Type u_2} [DecidableEq α] [Div α] (s : Finset α) :
                                  @[simp]
                                  theorem Finset.sub_eq_empty {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} :
                                  s - t = s = t =
                                  @[simp]
                                  theorem Finset.div_eq_empty {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} :
                                  s / t = s = t =
                                  @[simp]
                                  theorem Finset.sub_nonempty {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} :
                                  @[simp]
                                  theorem Finset.div_nonempty {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} :
                                  theorem Finset.Nonempty.sub {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} :
                                  theorem Finset.Nonempty.div {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} :
                                  theorem Finset.Nonempty.of_sub_left {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} :
                                  theorem Finset.Nonempty.of_div_left {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} :
                                  theorem Finset.Nonempty.of_sub_right {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} :
                                  theorem Finset.Nonempty.of_div_right {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} :
                                  @[simp]
                                  theorem Finset.sub_singleton {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} (a : α) :
                                  s - {a} = Finset.image (fun x => x - a) s
                                  @[simp]
                                  theorem Finset.div_singleton {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} (a : α) :
                                  s / {a} = Finset.image (fun x => x / a) s
                                  @[simp]
                                  theorem Finset.singleton_sub {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} (a : α) :
                                  {a} - s = Finset.image ((fun x x_1 => x - x_1) a) s
                                  @[simp]
                                  theorem Finset.singleton_div {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} (a : α) :
                                  {a} / s = Finset.image ((fun x x_1 => x / x_1) a) s
                                  theorem Finset.singleton_sub_singleton {α : Type u_2} [DecidableEq α] [Sub α] (a : α) (b : α) :
                                  {a} - {b} = {a - b}
                                  theorem Finset.singleton_div_singleton {α : Type u_2} [DecidableEq α] [Div α] (a : α) (b : α) :
                                  {a} / {b} = {a / b}
                                  theorem Finset.sub_subset_sub {α : Type u_2} [DecidableEq α] [Sub α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                                  s₁ s₂t₁ t₂s₁ - t₁ s₂ - t₂
                                  theorem Finset.div_subset_div {α : Type u_2} [DecidableEq α] [Div α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                                  s₁ s₂t₁ t₂s₁ / t₁ s₂ / t₂
                                  theorem Finset.sub_subset_sub_left {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                                  t₁ t₂s - t₁ s - t₂
                                  theorem Finset.div_subset_div_left {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                                  t₁ t₂s / t₁ s / t₂
                                  theorem Finset.sub_subset_sub_right {α : Type u_2} [DecidableEq α] [Sub α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
                                  s₁ s₂s₁ - t s₂ - t
                                  theorem Finset.div_subset_div_right {α : Type u_2} [DecidableEq α] [Div α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
                                  s₁ s₂s₁ / t s₂ / t
                                  theorem Finset.sub_subset_iff {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} {u : Finset α} :
                                  s - t u ∀ (x : α), x s∀ (y : α), y tx - y u
                                  theorem Finset.div_subset_iff {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} {u : Finset α} :
                                  s / t u ∀ (x : α), x s∀ (y : α), y tx / y u
                                  theorem Finset.union_sub {α : Type u_2} [DecidableEq α] [Sub α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
                                  s₁ s₂ - t = s₁ - t (s₂ - t)
                                  theorem Finset.union_div {α : Type u_2} [DecidableEq α] [Div α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
                                  (s₁ s₂) / t = s₁ / t s₂ / t
                                  theorem Finset.sub_union {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                                  s - (t₁ t₂) = s - t₁ (s - t₂)
                                  theorem Finset.div_union {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                                  s / (t₁ t₂) = s / t₁ s / t₂
                                  theorem Finset.inter_sub_subset {α : Type u_2} [DecidableEq α] [Sub α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
                                  s₁ s₂ - t (s₁ - t) (s₂ - t)
                                  theorem Finset.inter_div_subset {α : Type u_2} [DecidableEq α] [Div α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} :
                                  s₁ s₂ / t s₁ / t (s₂ / t)
                                  theorem Finset.sub_inter_subset {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                                  s - t₁ t₂ (s - t₁) (s - t₂)
                                  theorem Finset.div_inter_subset {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                                  s / (t₁ t₂) s / t₁ (s / t₂)
                                  theorem Finset.inter_sub_union_subset_union {α : Type u_2} [DecidableEq α] [Sub α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                                  s₁ s₂ - (t₁ t₂) s₁ - t₁ (s₂ - t₂)
                                  theorem Finset.inter_div_union_subset_union {α : Type u_2} [DecidableEq α] [Div α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                                  s₁ s₂ / (t₁ t₂) s₁ / t₁ s₂ / t₂
                                  theorem Finset.union_sub_inter_subset_union {α : Type u_2} [DecidableEq α] [Sub α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                                  s₁ s₂ - t₁ t₂ s₁ - t₁ (s₂ - t₂)
                                  theorem Finset.union_div_inter_subset_union {α : Type u_2} [DecidableEq α] [Div α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
                                  (s₁ s₂) / (t₁ t₂) s₁ / t₁ s₂ / t₂
                                  theorem Finset.subset_sub {α : Type u_2} [DecidableEq α] [Sub α] {u : Finset α} {s : Set α} {t : Set α} :
                                  u s - ts' t', s' s t' t u s' - t'

                                  If a finset u is contained in the sum of two sets s - t, we can find two finsets s', t' such that s' ⊆ s, t' ⊆ t and u ⊆ s' - t'.

                                  theorem Finset.subset_div {α : Type u_2} [DecidableEq α] [Div α] {u : Finset α} {s : Set α} {t : Set α} :
                                  u s / ts' t', s' s t' t u s' / t'

                                  If a finset u is contained in the product of two sets s / t, we can find two finsets s', t' such that s' ⊆ s, t' ⊆ t and u ⊆ s' / t'.

                                  Instances #

                                  def Finset.nsmul {α : Type u_2} [DecidableEq α] [Zero α] [Add α] :

                                  Repeated pointwise addition (not the same as pointwise repeated addition!) of a Finset. See note [pointwise nat action].

                                  Equations
                                  • Finset.nsmul = { smul := nsmulRec }
                                  Instances For
                                    def Finset.npow {α : Type u_2} [DecidableEq α] [One α] [Mul α] :

                                    Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a Finset. See note [pointwise nat action].

                                    Equations
                                    • Finset.npow = { pow := fun s n => npowRec n s }
                                    Instances For
                                      def Finset.zsmul {α : Type u_2} [DecidableEq α] [Zero α] [Add α] [Neg α] :

                                      Repeated pointwise addition/subtraction (not the same as pointwise repeated addition/subtraction!) of a Finset. See note [pointwise nat action].

                                      Equations
                                      • Finset.zsmul = { smul := zsmulRec }
                                      Instances For
                                        def Finset.zpow {α : Type u_2} [DecidableEq α] [One α] [Mul α] [Inv α] :

                                        Repeated pointwise multiplication/division (not the same as pointwise repeated multiplication/division!) of a Finset. See note [pointwise nat action].

                                        Equations
                                        • Finset.zpow = { pow := fun s n => zpowRec n s }
                                        Instances For
                                          theorem Finset.addSemigroup.proof_1 {α : Type u_1} [DecidableEq α] [AddSemigroup α] (s : Finset α) (t : Finset α) :
                                          ↑(s + t) = s + t

                                          Finset α is an AddSemigroup under pointwise operations if α is.

                                          Equations
                                          Instances For

                                            Finset α is a Semigroup under pointwise operations if α is.

                                            Equations
                                            Instances For
                                              theorem Finset.addCommSemigroup.proof_1 {α : Type u_1} [DecidableEq α] [AddCommSemigroup α] (s : Finset α) (t : Finset α) :
                                              ↑(s + t) = s + t

                                              Finset α is an AddCommSemigroup under pointwise operations if α is.

                                              Equations
                                              Instances For

                                                Finset α is a CommSemigroup under pointwise operations if α is.

                                                Equations
                                                Instances For
                                                  theorem Finset.inter_add_union_subset {α : Type u_2} [DecidableEq α] [AddCommSemigroup α] {s : Finset α} {t : Finset α} :
                                                  s t + (s t) s + t
                                                  theorem Finset.inter_mul_union_subset {α : Type u_2} [DecidableEq α] [CommSemigroup α] {s : Finset α} {t : Finset α} :
                                                  s t * (s t) s * t
                                                  theorem Finset.union_add_inter_subset {α : Type u_2} [DecidableEq α] [AddCommSemigroup α] {s : Finset α} {t : Finset α} :
                                                  s t + s t s + t
                                                  theorem Finset.union_mul_inter_subset {α : Type u_2} [DecidableEq α] [CommSemigroup α] {s : Finset α} {t : Finset α} :
                                                  (s t) * (s t) s * t
                                                  theorem Finset.addZeroClass.proof_2 {α : Type u_1} [DecidableEq α] [AddZeroClass α] (s : Finset α) (t : Finset α) :
                                                  ↑(s + t) = s + t
                                                  theorem Finset.addZeroClass.proof_1 {α : Type u_1} [AddZeroClass α] :
                                                  {0} = {0}

                                                  Finset α is an AddZeroClass under pointwise operations if α is.

                                                  Equations
                                                  Instances For

                                                    Finset α is a MulOneClass under pointwise operations if α is.

                                                    Equations
                                                    Instances For
                                                      theorem Finset.subset_add_left {α : Type u_2} [DecidableEq α] [AddZeroClass α] (s : Finset α) {t : Finset α} (ht : 0 t) :
                                                      s s + t
                                                      theorem Finset.subset_mul_left {α : Type u_2} [DecidableEq α] [MulOneClass α] (s : Finset α) {t : Finset α} (ht : 1 t) :
                                                      s s * t
                                                      theorem Finset.subset_add_right {α : Type u_2} [DecidableEq α] [AddZeroClass α] {s : Finset α} (t : Finset α) (hs : 0 s) :
                                                      t s + t
                                                      theorem Finset.subset_mul_right {α : Type u_2} [DecidableEq α] [MulOneClass α] {s : Finset α} (t : Finset α) (hs : 1 s) :
                                                      t s * t
                                                      theorem Finset.singletonAddMonoidHom.proof_2 {α : Type u_1} [DecidableEq α] [AddZeroClass α] (x : α) (y : α) :
                                                      AddHom.toFun Finset.singletonAddHom (x + y) = AddHom.toFun Finset.singletonAddHom x + AddHom.toFun Finset.singletonAddHom y
                                                      theorem Finset.singletonAddMonoidHom.proof_1 {α : Type u_1} [AddZeroClass α] :
                                                      ZeroHom.toFun Finset.singletonZeroHom 0 = 0

                                                      The singleton operation as an AddMonoidHom.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For

                                                        The singleton operation as a MonoidHom.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          @[simp]
                                                          theorem Finset.coe_singletonAddMonoidHom {α : Type u_2} [DecidableEq α] [AddZeroClass α] :
                                                          Finset.singletonAddMonoidHom = singleton
                                                          @[simp]
                                                          theorem Finset.coe_singletonMonoidHom {α : Type u_2} [DecidableEq α] [MulOneClass α] :
                                                          Finset.singletonMonoidHom = singleton
                                                          @[simp]
                                                          theorem Finset.singletonAddMonoidHom_apply {α : Type u_2} [DecidableEq α] [AddZeroClass α] (a : α) :
                                                          Finset.singletonAddMonoidHom a = {a}
                                                          @[simp]
                                                          theorem Finset.singletonMonoidHom_apply {α : Type u_2} [DecidableEq α] [MulOneClass α] (a : α) :
                                                          Finset.singletonMonoidHom a = {a}
                                                          theorem Finset.coeAddMonoidHom.proof_2 {α : Type u_1} [DecidableEq α] [AddZeroClass α] (s : Finset α) (t : Finset α) :
                                                          ↑(s + t) = s + t
                                                          noncomputable def Finset.coeAddMonoidHom {α : Type u_2} [DecidableEq α] [AddZeroClass α] :

                                                          The coercion from Finset to set as an AddMonoidHom.

                                                          Equations
                                                          • Finset.coeAddMonoidHom = { toZeroHom := { toFun := CoeTC.coe, map_zero' := (_ : 0 = 0) }, map_add' := (_ : ∀ (s t : Finset α), ↑(s + t) = s + t) }
                                                          Instances For
                                                            noncomputable def Finset.coeMonoidHom {α : Type u_2} [DecidableEq α] [MulOneClass α] :

                                                            The coercion from Finset to Set as a MonoidHom.

                                                            Equations
                                                            • Finset.coeMonoidHom = { toOneHom := { toFun := CoeTC.coe, map_one' := (_ : 1 = 1) }, map_mul' := (_ : ∀ (s t : Finset α), ↑(s * t) = s * t) }
                                                            Instances For
                                                              @[simp]
                                                              theorem Finset.coe_coeAddMonoidHom {α : Type u_2} [DecidableEq α] [AddZeroClass α] :
                                                              Finset.coeAddMonoidHom = CoeTC.coe
                                                              @[simp]
                                                              theorem Finset.coe_coeMonoidHom {α : Type u_2} [DecidableEq α] [MulOneClass α] :
                                                              Finset.coeMonoidHom = CoeTC.coe
                                                              @[simp]
                                                              theorem Finset.coeAddMonoidHom_apply {α : Type u_2} [DecidableEq α] [AddZeroClass α] (s : Finset α) :
                                                              Finset.coeAddMonoidHom s = s
                                                              @[simp]
                                                              theorem Finset.coeMonoidHom_apply {α : Type u_2} [DecidableEq α] [MulOneClass α] (s : Finset α) :
                                                              Finset.coeMonoidHom s = s
                                                              theorem Finset.imageAddMonoidHom.proof_1 {F : Type u_3} {α : Type u_2} {β : Type u_1} [DecidableEq β] [AddZeroClass α] [AddZeroClass β] [AddMonoidHomClass F α β] (f : F) :
                                                              def Finset.imageAddMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [AddZeroClass α] [AddZeroClass β] [AddMonoidHomClass F α β] (f : F) :

                                                              Lift an add_monoid_hom to Finset via image

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                @[simp]
                                                                theorem Finset.imageAddMonoidHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [AddZeroClass α] [AddZeroClass β] [AddMonoidHomClass F α β] (f : F) :
                                                                @[simp]
                                                                theorem Finset.imageMonoidHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [MulOneClass α] [MulOneClass β] [MonoidHomClass F α β] (f : F) :
                                                                def Finset.imageMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [MulOneClass α] [MulOneClass β] [MonoidHomClass F α β] (f : F) :

                                                                Lift a MonoidHom to Finset via image.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  @[simp]
                                                                  theorem Finset.coe_nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] (s : Finset α) (n : ) :
                                                                  ↑(n s) = n s
                                                                  @[simp]
                                                                  theorem Finset.coe_pow {α : Type u_2} [DecidableEq α] [Monoid α] (s : Finset α) (n : ) :
                                                                  ↑(s ^ n) = s ^ n

                                                                  Finset α is an AddMonoid under pointwise operations if α is.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    theorem Finset.addMonoid.proof_1 {α : Type u_1} [AddMonoid α] :
                                                                    0 = 0
                                                                    theorem Finset.addMonoid.proof_2 {α : Type u_1} [DecidableEq α] [AddMonoid α] (s : Finset α) (t : Finset α) :
                                                                    ↑(s + t) = s + t
                                                                    theorem Finset.addMonoid.proof_3 {α : Type u_1} [DecidableEq α] [AddMonoid α] (s : Finset α) (n : ) :
                                                                    ↑(n s) = n s
                                                                    def Finset.monoid {α : Type u_2} [DecidableEq α] [Monoid α] :

                                                                    Finset α is a Monoid under pointwise operations if α is.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      abbrev Finset.nsmul_mem_nsmul.match_1 (motive : Prop) :
                                                                      (x : ) → (Unitmotive 0) → ((n : ) → motive (Nat.succ n)) → motive x
                                                                      Equations
                                                                      Instances For
                                                                        theorem Finset.nsmul_mem_nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {a : α} (ha : a s) (n : ) :
                                                                        n a n s
                                                                        theorem Finset.pow_mem_pow {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {a : α} (ha : a s) (n : ) :
                                                                        a ^ n s ^ n
                                                                        theorem Finset.nsmul_subset_nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {t : Finset α} (hst : s t) (n : ) :
                                                                        n s n t
                                                                        theorem Finset.pow_subset_pow {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {t : Finset α} (hst : s t) (n : ) :
                                                                        s ^ n t ^ n
                                                                        theorem Finset.nsmul_subset_nsmul_of_zero_mem {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {m : } {n : } (hs : 0 s) :
                                                                        m nm s n s
                                                                        theorem Finset.pow_subset_pow_of_one_mem {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {m : } {n : } (hs : 1 s) :
                                                                        m ns ^ m s ^ n
                                                                        @[simp]
                                                                        theorem Finset.coe_list_sum {α : Type u_2} [DecidableEq α] [AddMonoid α] (s : List (Finset α)) :
                                                                        ↑(List.sum s) = List.sum (List.map Finset.toSet s)
                                                                        @[simp]
                                                                        theorem Finset.coe_list_prod {α : Type u_2} [DecidableEq α] [Monoid α] (s : List (Finset α)) :
                                                                        ↑(List.prod s) = List.prod (List.map Finset.toSet s)
                                                                        theorem Finset.mem_sum_list_ofFn {α : Type u_2} [DecidableEq α] [AddMonoid α] {n : } {a : α} {s : Fin nFinset α} :
                                                                        a List.sum (List.ofFn s) f, List.sum (List.ofFn fun i => ↑(f i)) = a
                                                                        theorem Finset.mem_prod_list_ofFn {α : Type u_2} [DecidableEq α] [Monoid α] {n : } {a : α} {s : Fin nFinset α} :
                                                                        a List.prod (List.ofFn s) f, List.prod (List.ofFn fun i => ↑(f i)) = a
                                                                        theorem Finset.mem_nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {a : α} {n : } :
                                                                        a n s f, List.sum (List.ofFn fun i => ↑(f i)) = a
                                                                        theorem Finset.mem_pow {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {a : α} {n : } :
                                                                        a s ^ n f, List.prod (List.ofFn fun i => ↑(f i)) = a
                                                                        @[simp]
                                                                        theorem Finset.empty_nsmul {α : Type u_2} [DecidableEq α] [AddMonoid α] {n : } (hn : n 0) :
                                                                        @[simp]
                                                                        theorem Finset.empty_pow {α : Type u_2} [DecidableEq α] [Monoid α] {n : } (hn : n 0) :
                                                                        theorem Finset.add_univ_of_zero_mem {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} [Fintype α] (hs : 0 s) :
                                                                        s + Finset.univ = Finset.univ
                                                                        theorem Finset.mul_univ_of_one_mem {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} [Fintype α] (hs : 1 s) :
                                                                        s * Finset.univ = Finset.univ
                                                                        theorem Finset.univ_add_of_zero_mem {α : Type u_2} [DecidableEq α] [AddMonoid α] {t : Finset α} [Fintype α] (ht : 0 t) :
                                                                        Finset.univ + t = Finset.univ
                                                                        theorem Finset.univ_mul_of_one_mem {α : Type u_2} [DecidableEq α] [Monoid α] {t : Finset α} [Fintype α] (ht : 1 t) :
                                                                        Finset.univ * t = Finset.univ
                                                                        @[simp]
                                                                        theorem Finset.univ_add_univ {α : Type u_2} [DecidableEq α] [AddMonoid α] [Fintype α] :
                                                                        Finset.univ + Finset.univ = Finset.univ
                                                                        @[simp]
                                                                        theorem Finset.univ_mul_univ {α : Type u_2} [DecidableEq α] [Monoid α] [Fintype α] :
                                                                        Finset.univ * Finset.univ = Finset.univ
                                                                        @[simp]
                                                                        theorem Finset.nsmul_univ {α : Type u_2} [DecidableEq α] [AddMonoid α] {n : } [Fintype α] (hn : n 0) :
                                                                        n Finset.univ = Finset.univ
                                                                        @[simp]
                                                                        theorem Finset.univ_pow {α : Type u_2} [DecidableEq α] [Monoid α] {n : } [Fintype α] (hn : n 0) :
                                                                        Finset.univ ^ n = Finset.univ
                                                                        theorem IsAddUnit.finset {α : Type u_2} [DecidableEq α] [AddMonoid α] {a : α} :
                                                                        theorem IsUnit.finset {α : Type u_2} [DecidableEq α] [Monoid α] {a : α} :
                                                                        IsUnit aIsUnit {a}
                                                                        theorem Finset.addCommMonoid.proof_2 {α : Type u_1} [DecidableEq α] [AddCommMonoid α] (s : Finset α) (t : Finset α) :
                                                                        ↑(s + t) = s + t
                                                                        theorem Finset.addCommMonoid.proof_3 {α : Type u_1} [DecidableEq α] [AddCommMonoid α] (s : Finset α) (n : ) :
                                                                        ↑(n s) = n s
                                                                        theorem Finset.addCommMonoid.proof_1 {α : Type u_1} [AddCommMonoid α] :
                                                                        0 = 0

                                                                        Finset α is an AddCommMonoid under pointwise operations if α is.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For

                                                                          Finset α is a CommMonoid under pointwise operations if α is.

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem Finset.coe_sum {α : Type u_2} [DecidableEq α] [AddCommMonoid α] {ι : Type u_5} (s : Finset ι) (f : ιFinset α) :
                                                                            ↑(Finset.sum s fun i => f i) = Finset.sum s fun i => ↑(f i)
                                                                            @[simp]
                                                                            theorem Finset.coe_prod {α : Type u_2} [DecidableEq α] [CommMonoid α] {ι : Type u_5} (s : Finset ι) (f : ιFinset α) :
                                                                            ↑(Finset.prod s fun i => f i) = Finset.prod s fun i => ↑(f i)
                                                                            @[simp]
                                                                            theorem Finset.coe_zsmul {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] (s : Finset α) (n : ) :
                                                                            ↑(n s) = n s
                                                                            abbrev Finset.coe_zsmul.match_1 (motive : Prop) :
                                                                            (x : ) → ((n : ) → motive (Int.ofNat n)) → ((n : ) → motive (Int.negSucc n)) → motive x
                                                                            Equations
                                                                            Instances For
                                                                              @[simp]
                                                                              theorem Finset.coe_zpow {α : Type u_2} [DecidableEq α] [DivisionMonoid α] (s : Finset α) (n : ) :
                                                                              ↑(s ^ n) = s ^ n
                                                                              theorem Finset.add_eq_zero_iff {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] {s : Finset α} {t : Finset α} :
                                                                              s + t = 0 a b, s = {a} t = {b} a + b = 0
                                                                              theorem Finset.mul_eq_one_iff {α : Type u_2} [DecidableEq α] [DivisionMonoid α] {s : Finset α} {t : Finset α} :
                                                                              s * t = 1 a b, s = {a} t = {b} a * b = 1
                                                                              theorem Finset.subtractionMonoid.proof_4 {α : Type u_1} [DecidableEq α] [SubtractionMonoid α] (s : Finset α) (t : Finset α) :
                                                                              ↑(s - t) = s - t

                                                                              Finset α is a subtraction monoid under pointwise operations if α is.

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                theorem Finset.subtractionMonoid.proof_3 {α : Type u_1} [DecidableEq α] [SubtractionMonoid α] (s : Finset α) :
                                                                                ↑(-s) = -s
                                                                                theorem Finset.subtractionMonoid.proof_2 {α : Type u_1} [DecidableEq α] [SubtractionMonoid α] (s : Finset α) (t : Finset α) :
                                                                                ↑(s + t) = s + t
                                                                                theorem Finset.subtractionMonoid.proof_6 {α : Type u_1} [DecidableEq α] [SubtractionMonoid α] (s : Finset α) (n : ) :
                                                                                ↑(n s) = n s
                                                                                theorem Finset.subtractionMonoid.proof_5 {α : Type u_1} [DecidableEq α] [SubtractionMonoid α] (s : Finset α) (n : ) :
                                                                                ↑(n s) = n s

                                                                                Finset α is a division monoid under pointwise operations if α is.

                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  @[simp]
                                                                                  theorem Finset.isAddUnit_iff {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] {s : Finset α} :
                                                                                  IsAddUnit s a, s = {a} IsAddUnit a
                                                                                  @[simp]
                                                                                  theorem Finset.isUnit_iff {α : Type u_2} [DecidableEq α] [DivisionMonoid α] {s : Finset α} :
                                                                                  IsUnit s a, s = {a} IsUnit a
                                                                                  @[simp]
                                                                                  theorem Finset.isAddUnit_coe {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] {s : Finset α} :
                                                                                  @[simp]
                                                                                  theorem Finset.isUnit_coe {α : Type u_2} [DecidableEq α] [DivisionMonoid α] {s : Finset α} :
                                                                                  theorem Finset.subtractionCommMonoid.proof_6 {α : Type u_1} [DecidableEq α] [SubtractionCommMonoid α] (s : Finset α) (n : ) :
                                                                                  ↑(n s) = n s
                                                                                  theorem Finset.subtractionCommMonoid.proof_4 {α : Type u_1} [DecidableEq α] [SubtractionCommMonoid α] (s : Finset α) (t : Finset α) :
                                                                                  ↑(s - t) = s - t

                                                                                  Finset α is a commutative subtraction monoid under pointwise operations if α is.

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    theorem Finset.subtractionCommMonoid.proof_5 {α : Type u_1} [DecidableEq α] [SubtractionCommMonoid α] (s : Finset α) (n : ) :
                                                                                    ↑(n s) = n s
                                                                                    theorem Finset.subtractionCommMonoid.proof_2 {α : Type u_1} [DecidableEq α] [SubtractionCommMonoid α] (s : Finset α) (t : Finset α) :
                                                                                    ↑(s + t) = s + t

                                                                                    Finset α is a commutative division monoid under pointwise operations if α is.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For

                                                                                      Finset α has distributive negation if α has.

                                                                                      Equations
                                                                                      Instances For

                                                                                        Note that Finset α is not a Distrib because s * t + s * u has cross terms that s * (t + u) lacks.

                                                                                        -- {10, 16, 18, 20, 8, 9}
                                                                                        #eval {1, 2} * ({3, 4} + {5, 6} : Finset ℕ)
                                                                                        
                                                                                        -- {10, 11, 12, 13, 14, 15, 16, 18, 20, 8, 9}
                                                                                        #eval ({1, 2} : Finset ℕ) * {3, 4} + {1, 2} * {5, 6}
                                                                                        
                                                                                        theorem Finset.mul_add_subset {α : Type u_2} [DecidableEq α] [Distrib α] (s : Finset α) (t : Finset α) (u : Finset α) :
                                                                                        s * (t + u) s * t + s * u
                                                                                        theorem Finset.add_mul_subset {α : Type u_2} [DecidableEq α] [Distrib α] (s : Finset α) (t : Finset α) (u : Finset α) :
                                                                                        (s + t) * u s * u + t * u

                                                                                        Note that Finset is not a MulZeroClass because 0 * ∅ ≠ 0.

                                                                                        theorem Finset.mul_zero_subset {α : Type u_2} [DecidableEq α] [MulZeroClass α] (s : Finset α) :
                                                                                        s * 0 0
                                                                                        theorem Finset.zero_mul_subset {α : Type u_2} [DecidableEq α] [MulZeroClass α] (s : Finset α) :
                                                                                        0 * s 0
                                                                                        theorem Finset.Nonempty.mul_zero {α : Type u_2} [DecidableEq α] [MulZeroClass α] {s : Finset α} (hs : Finset.Nonempty s) :
                                                                                        s * 0 = 0
                                                                                        theorem Finset.Nonempty.zero_mul {α : Type u_2} [DecidableEq α] [MulZeroClass α] {s : Finset α} (hs : Finset.Nonempty s) :
                                                                                        0 * s = 0

                                                                                        Note that Finset is not a Group because s / s ≠ 1 in general.

                                                                                        @[simp]
                                                                                        theorem Finset.zero_mem_sub_iff {α : Type u_2} [DecidableEq α] [AddGroup α] {s : Finset α} {t : Finset α} :
                                                                                        0 s - t ¬Disjoint s t
                                                                                        @[simp]
                                                                                        theorem Finset.one_mem_div_iff {α : Type u_2} [DecidableEq α] [Group α] {s : Finset α} {t : Finset α} :
                                                                                        1 s / t ¬Disjoint s t
                                                                                        theorem Finset.not_zero_mem_sub_iff {α : Type u_2} [DecidableEq α] [AddGroup α] {s : Finset α} {t : Finset α} :
                                                                                        ¬0 s - t Disjoint s t
                                                                                        theorem Finset.not_one_mem_div_iff {α : Type u_2} [DecidableEq α] [Group α] {s : Finset α} {t : Finset α} :
                                                                                        ¬1 s / t Disjoint s t
                                                                                        theorem Finset.Nonempty.zero_mem_sub {α : Type u_2} [DecidableEq α] [AddGroup α] {s : Finset α} (h : Finset.Nonempty s) :
                                                                                        0 s - s
                                                                                        abbrev Finset.Nonempty.zero_mem_sub.match_1 {α : Type u_1} {s : Finset α} (motive : Finset.Nonempty sProp) :
                                                                                        (h : Finset.Nonempty s) → ((a : α) → (ha : a s) → motive (_ : x, x s)) → motive h
                                                                                        Equations
                                                                                        Instances For
                                                                                          theorem Finset.Nonempty.one_mem_div {α : Type u_2} [DecidableEq α] [Group α] {s : Finset α} (h : Finset.Nonempty s) :
                                                                                          1 s / s
                                                                                          theorem Finset.isAddUnit_singleton {α : Type u_2} [DecidableEq α] [AddGroup α] (a : α) :
                                                                                          theorem Finset.isUnit_singleton {α : Type u_2} [DecidableEq α] [Group α] (a : α) :
                                                                                          IsUnit {a}
                                                                                          theorem Finset.isUnit_iff_singleton {α : Type u_2} [DecidableEq α] [Group α] {s : Finset α} :
                                                                                          IsUnit s a, s = {a}
                                                                                          @[simp]
                                                                                          theorem Finset.isUnit_iff_singleton_aux {α : Type u_2} [Group α] {s : Finset α} :
                                                                                          (a, s = {a} IsUnit a) a, s = {a}
                                                                                          @[simp]
                                                                                          theorem Finset.image_add_left {α : Type u_2} [DecidableEq α] [AddGroup α] {t : Finset α} {a : α} :
                                                                                          Finset.image (fun b => a + b) t = Finset.preimage t (fun b => -a + b) (_ : Set.InjOn ((fun x x_1 => x + x_1) (-a)) ((fun b => -a + b) ⁻¹' t))
                                                                                          @[simp]
                                                                                          theorem Finset.image_mul_left {α : Type u_2} [DecidableEq α] [Group α] {t : Finset α} {a : α} :
                                                                                          Finset.image (fun b => a * b) t = Finset.preimage t (fun b => a⁻¹ * b) (_ : Set.InjOn ((fun x x_1 => x * x_1) a⁻¹) ((fun b => a⁻¹ * b) ⁻¹' t))
                                                                                          @[simp]
                                                                                          theorem Finset.image_add_right {α : Type u_2} [DecidableEq α] [AddGroup α] {t : Finset α} {b : α} :
                                                                                          Finset.image (fun x => x + b) t = Finset.preimage t (fun x => x + -b) (_ : Set.InjOn (fun x => x + -b) ((fun x => x + -b) ⁻¹' t))
                                                                                          @[simp]
                                                                                          theorem Finset.image_mul_right {α : Type u_2} [DecidableEq α] [Group α] {t : Finset α} {b : α} :
                                                                                          Finset.image (fun x => x * b) t = Finset.preimage t (fun x => x * b⁻¹) (_ : Set.InjOn (fun x => x * b⁻¹) ((fun x => x * b⁻¹) ⁻¹' t))
                                                                                          theorem Finset.image_add_left' {α : Type u_2} [DecidableEq α] [AddGroup α] {t : Finset α} {a : α} :
                                                                                          Finset.image (fun b => -a + b) t = Finset.preimage t (fun b => a + b) (_ : Set.InjOn ((fun x x_1 => x + x_1) a) ((fun b => a + b) ⁻¹' t))
                                                                                          theorem Finset.image_mul_left' {α : Type u_2} [DecidableEq α] [Group α] {t : Finset α} {a : α} :
                                                                                          Finset.image (fun b => a⁻¹ * b) t = Finset.preimage t (fun b => a * b) (_ : Set.InjOn ((fun x x_1 => x * x_1) a) ((fun b => a * b) ⁻¹' t))
                                                                                          theorem Finset.image_add_right' {α : Type u_2} [DecidableEq α] [AddGroup α] {t : Finset α} {b : α} :
                                                                                          Finset.image (fun x => x + -b) t = Finset.preimage t (fun x => x + b) (_ : Set.InjOn (fun x => x + b) ((fun x => x + b) ⁻¹' t))
                                                                                          theorem Finset.image_mul_right' {α : Type u_2} [DecidableEq α] [Group α] {t : Finset α} {b : α} :
                                                                                          Finset.image (fun x => x * b⁻¹) t = Finset.preimage t (fun x => x * b) (_ : Set.InjOn (fun x => x * b) ((fun x => x * b) ⁻¹' t))
                                                                                          theorem Finset.image_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Group α] [DivisionMonoid β] [MonoidHomClass F α β] (f : F) {s : Finset α} {t : Finset α} :
                                                                                          Finset.image (f) (s / t) = Finset.image (f) s / Finset.image (f) t
                                                                                          theorem Finset.div_zero_subset {α : Type u_2} [DecidableEq α] [GroupWithZero α] (s : Finset α) :
                                                                                          s / 0 0
                                                                                          theorem Finset.zero_div_subset {α : Type u_2} [DecidableEq α] [GroupWithZero α] (s : Finset α) :
                                                                                          0 / s 0
                                                                                          theorem Finset.Nonempty.div_zero {α : Type u_2} [DecidableEq α] [GroupWithZero α] {s : Finset α} (hs : Finset.Nonempty s) :
                                                                                          s / 0 = 0
                                                                                          theorem Finset.Nonempty.zero_div {α : Type u_2} [DecidableEq α] [GroupWithZero α] {s : Finset α} (hs : Finset.Nonempty s) :
                                                                                          0 / s = 0
                                                                                          @[simp]
                                                                                          theorem Finset.preimage_add_left_singleton {α : Type u_2} [AddGroup α] {a : α} {b : α} :
                                                                                          Finset.preimage {b} ((fun x x_1 => x + x_1) a) (_ : Set.InjOn ((fun x x_1 => x + x_1) a) ((fun x x_1 => x + x_1) a ⁻¹' {b})) = {-a + b}
                                                                                          @[simp]
                                                                                          theorem Finset.preimage_mul_left_singleton {α : Type u_2} [Group α] {a : α} {b : α} :
                                                                                          Finset.preimage {b} ((fun x x_1 => x * x_1) a) (_ : Set.InjOn ((fun x x_1 => x * x_1) a) ((fun x x_1 => x * x_1) a ⁻¹' {b})) = {a⁻¹ * b}
                                                                                          @[simp]
                                                                                          theorem Finset.preimage_add_right_singleton {α : Type u_2} [AddGroup α] {a : α} {b : α} :
                                                                                          Finset.preimage {b} (fun x => x + a) (_ : Set.InjOn (fun x => x + a) ((fun x => x + a) ⁻¹' {b})) = {b + -a}
                                                                                          @[simp]
                                                                                          theorem Finset.preimage_mul_right_singleton {α : Type u_2} [Group α] {a : α} {b : α} :
                                                                                          Finset.preimage {b} (fun x => x * a) (_ : Set.InjOn (fun x => x * a) ((fun x => x * a) ⁻¹' {b})) = {b * a⁻¹}
                                                                                          @[simp]
                                                                                          theorem Finset.preimage_add_left_zero {α : Type u_2} [AddGroup α] {a : α} :
                                                                                          Finset.preimage 0 ((fun x x_1 => x + x_1) a) (_ : Set.InjOn ((fun x x_1 => x + x_1) a) ((fun x x_1 => x + x_1) a ⁻¹' 0)) = {-a}
                                                                                          @[simp]
                                                                                          theorem Finset.preimage_mul_left_one {α : Type u_2} [Group α] {a : α} :
                                                                                          Finset.preimage 1 ((fun x x_1 => x * x_1) a) (_ : Set.InjOn ((fun x x_1 => x * x_1) a) ((fun x x_1 => x * x_1) a ⁻¹' 1)) = {a⁻¹}
                                                                                          @[simp]
                                                                                          theorem Finset.preimage_add_right_zero {α : Type u_2} [AddGroup α] {b : α} :
                                                                                          Finset.preimage 0 (fun x => x + b) (_ : Set.InjOn (fun x => x + b) ((fun x => x + b) ⁻¹' 0)) = {-b}
                                                                                          @[simp]
                                                                                          theorem Finset.preimage_mul_right_one {α : Type u_2} [Group α] {b : α} :
                                                                                          Finset.preimage 1 (fun x => x * b) (_ : Set.InjOn (fun x => x * b) ((fun x => x * b) ⁻¹' 1)) = {b⁻¹}
                                                                                          theorem Finset.preimage_add_left_zero' {α : Type u_2} [AddGroup α] {a : α} :
                                                                                          Finset.preimage 0 ((fun x x_1 => x + x_1) (-a)) (_ : Set.InjOn ((fun x x_1 => x + x_1) (-a)) ((fun x x_1 => x + x_1) (-a) ⁻¹' 0)) = {a}
                                                                                          theorem Finset.preimage_mul_left_one' {α : Type u_2} [Group α] {a : α} :
                                                                                          Finset.preimage 1 ((fun x x_1 => x * x_1) a⁻¹) (_ : Set.InjOn ((fun x x_1 => x * x_1) a⁻¹) ((fun x x_1 => x * x_1) a⁻¹ ⁻¹' 1)) = {a}
                                                                                          theorem Finset.preimage_add_right_zero' {α : Type u_2} [AddGroup α] {b : α} :
                                                                                          Finset.preimage 0 (fun x => x + -b) (_ : Set.InjOn (fun x => x + -b) ((fun x => x + -b) ⁻¹' 0)) = {b}
                                                                                          theorem Finset.preimage_mul_right_one' {α : Type u_2} [Group α] {b : α} :
                                                                                          Finset.preimage 1 (fun x => x * b⁻¹) (_ : Set.InjOn (fun x => x * b⁻¹) ((fun x => x * b⁻¹) ⁻¹' 1)) = {b}

                                                                                          Scalar addition/multiplication of finsets #

                                                                                          def Finset.vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] :
                                                                                          VAdd (Finset α) (Finset β)

                                                                                          The pointwise sum of two finsets s and t: s +ᵥ t = {x +ᵥ y | x ∈ s, y ∈ t}.

                                                                                          Equations
                                                                                          Instances For
                                                                                            def Finset.smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] :
                                                                                            SMul (Finset α) (Finset β)

                                                                                            The pointwise product of two finsets s and t: s • t = {x • y | x ∈ s, y ∈ t}.

                                                                                            Equations
                                                                                            Instances For
                                                                                              theorem Finset.vadd_def {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} :
                                                                                              s +ᵥ t = Finset.image (fun p => p.fst +ᵥ p.snd) (s ×ˢ t)
                                                                                              theorem Finset.smul_def {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} :
                                                                                              s t = Finset.image (fun p => p.fst p.snd) (s ×ˢ t)
                                                                                              theorem Finset.image_vadd_product {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} :
                                                                                              Finset.image (fun x => x.fst +ᵥ x.snd) (s ×ˢ t) = s +ᵥ t
                                                                                              theorem Finset.image_smul_product {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} :
                                                                                              Finset.image (fun x => x.fst x.snd) (s ×ˢ t) = s t
                                                                                              theorem Finset.mem_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} {x : β} :
                                                                                              x s +ᵥ t y z, y s z t y +ᵥ z = x
                                                                                              theorem Finset.mem_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} {x : β} :
                                                                                              x s t y z, y s z t y z = x
                                                                                              @[simp]
                                                                                              theorem Finset.coe_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (s : Finset α) (t : Finset β) :
                                                                                              ↑(s +ᵥ t) = s +ᵥ t
                                                                                              @[simp]
                                                                                              theorem Finset.coe_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (s : Finset α) (t : Finset β) :
                                                                                              ↑(s t) = s t
                                                                                              theorem Finset.vadd_mem_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} {a : α} {b : β} :
                                                                                              a sb ta +ᵥ b s +ᵥ t
                                                                                              theorem Finset.smul_mem_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} {a : α} {b : β} :
                                                                                              a sb ta b s t
                                                                                              theorem Finset.vadd_card_le {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} :
                                                                                              theorem Finset.smul_card_le {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} :
                                                                                              @[simp]
                                                                                              theorem Finset.empty_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (t : Finset β) :
                                                                                              @[simp]
                                                                                              theorem Finset.empty_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (t : Finset β) :
                                                                                              @[simp]
                                                                                              theorem Finset.vadd_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (s : Finset α) :
                                                                                              @[simp]
                                                                                              theorem Finset.smul_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (s : Finset α) :
                                                                                              @[simp]
                                                                                              theorem Finset.vadd_eq_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} :
                                                                                              s +ᵥ t = s = t =
                                                                                              @[simp]
                                                                                              theorem Finset.smul_eq_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} :
                                                                                              s t = s = t =
                                                                                              @[simp]
                                                                                              theorem Finset.vadd_nonempty_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} :
                                                                                              @[simp]
                                                                                              theorem Finset.smul_nonempty_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} :
                                                                                              theorem Finset.Nonempty.vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} :
                                                                                              theorem Finset.Nonempty.smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} :
                                                                                              theorem Finset.Nonempty.of_vadd_left {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} :
                                                                                              theorem Finset.Nonempty.of_smul_left {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} :
                                                                                              theorem Finset.Nonempty.of_vadd_right {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} :
                                                                                              theorem Finset.Nonempty.of_smul_right {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} :
                                                                                              theorem Finset.vadd_singleton {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} (b : β) :
                                                                                              s +ᵥ {b} = Finset.image (fun x => x +ᵥ b) s
                                                                                              theorem Finset.smul_singleton {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} (b : β) :
                                                                                              s {b} = Finset.image (fun x => x b) s
                                                                                              theorem Finset.singleton_vadd_singleton {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (a : α) (b : β) :
                                                                                              {a} +ᵥ {b} = {a +ᵥ b}
                                                                                              theorem Finset.singleton_smul_singleton {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (a : α) (b : β) :
                                                                                              {a} {b} = {a b}
                                                                                              theorem Finset.vadd_subset_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset β} {t₂ : Finset β} :
                                                                                              s₁ s₂t₁ t₂s₁ +ᵥ t₁ s₂ +ᵥ t₂
                                                                                              theorem Finset.smul_subset_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset β} {t₂ : Finset β} :
                                                                                              s₁ s₂t₁ t₂s₁ t₁ s₂ t₂
                                                                                              theorem Finset.vadd_subset_vadd_left {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t₁ : Finset β} {t₂ : Finset β} :
                                                                                              t₁ t₂s +ᵥ t₁ s +ᵥ t₂
                                                                                              theorem Finset.smul_subset_smul_left {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t₁ : Finset β} {t₂ : Finset β} :
                                                                                              t₁ t₂s t₁ s t₂
                                                                                              theorem Finset.vadd_subset_vadd_right {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s₁ : Finset α} {s₂ : Finset α} {t : Finset β} :
                                                                                              s₁ s₂s₁ +ᵥ t s₂ +ᵥ t
                                                                                              theorem Finset.smul_subset_smul_right {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s₁ : Finset α} {s₂ : Finset α} {t : Finset β} :
                                                                                              s₁ s₂s₁ t s₂ t
                                                                                              theorem Finset.vadd_subset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} {u : Finset β} :
                                                                                              s +ᵥ t u ∀ (a : α), a s∀ (b : β), b ta +ᵥ b u
                                                                                              theorem Finset.smul_subset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} {u : Finset β} :
                                                                                              s t u ∀ (a : α), a s∀ (b : β), b ta b u
                                                                                              theorem Finset.union_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s₁ : Finset α} {s₂ : Finset α} {t : Finset β} [DecidableEq α] :
                                                                                              s₁ s₂ +ᵥ t = s₁ +ᵥ t (s₂ +ᵥ t)
                                                                                              theorem Finset.union_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s₁ : Finset α} {s₂ : Finset α} {t : Finset β} [DecidableEq α] :
                                                                                              (s₁ s₂) t = s₁ t s₂ t
                                                                                              theorem Finset.vadd_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t₁ : Finset β} {t₂ : Finset β} :
                                                                                              s +ᵥ (t₁ t₂) = s +ᵥ t₁ (s +ᵥ t₂)
                                                                                              theorem Finset.smul_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t₁ : Finset β} {t₂ : Finset β} :
                                                                                              s (t₁ t₂) = s t₁ s t₂
                                                                                              theorem Finset.inter_vadd_subset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s₁ : Finset α} {s₂ : Finset α} {t : Finset β} [DecidableEq α] :
                                                                                              s₁ s₂ +ᵥ t (s₁ +ᵥ t) (s₂ +ᵥ t)
                                                                                              theorem Finset.inter_smul_subset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s₁ : Finset α} {s₂ : Finset α} {t : Finset β} [DecidableEq α] :
                                                                                              (s₁ s₂) t s₁ t s₂ t
                                                                                              theorem Finset.vadd_inter_subset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t₁ : Finset β} {t₂ : Finset β} :
                                                                                              s +ᵥ t₁ t₂ (s +ᵥ t₁) (s +ᵥ t₂)
                                                                                              theorem Finset.smul_inter_subset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t₁ : Finset β} {t₂ : Finset β} :
                                                                                              s (t₁ t₂) s t₁ s t₂
                                                                                              theorem Finset.inter_vadd_union_subset_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset β} {t₂ : Finset β} [DecidableEq α] :
                                                                                              s₁ s₂ +ᵥ (t₁ t₂) s₁ +ᵥ t₁ (s₂ +ᵥ t₂)
                                                                                              theorem Finset.inter_smul_union_subset_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset β} {t₂ : Finset β} [DecidableEq α] :
                                                                                              (s₁ s₂) (t₁ t₂) s₁ t₁ s₂ t₂
                                                                                              theorem Finset.union_vadd_inter_subset_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset β} {t₂ : Finset β} [DecidableEq α] :
                                                                                              s₁ s₂ +ᵥ t₁ t₂ s₁ +ᵥ t₁ (s₂ +ᵥ t₂)
                                                                                              theorem Finset.union_smul_inter_subset_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset β} {t₂ : Finset β} [DecidableEq α] :
                                                                                              (s₁ s₂) (t₁ t₂) s₁ t₁ s₂ t₂
                                                                                              theorem Finset.subset_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {u : Finset β} {s : Set α} {t : Set β} :
                                                                                              u s +ᵥ ts' t', s' s t' t u s' +ᵥ t'

                                                                                              If a finset u is contained in the scalar sum of two sets s +ᵥ t, we can find two finsets s', t' such that s' ⊆ s, t' ⊆ t and u ⊆ s' +ᵥ t'.

                                                                                              theorem Finset.subset_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {u : Finset β} {s : Set α} {t : Set β} :
                                                                                              u s ts' t', s' s t' t u s' t'

                                                                                              If a finset u is contained in the scalar product of two sets s • t, we can find two finsets s', t' such that s' ⊆ s, t' ⊆ t and u ⊆ s' • t'.

                                                                                              Scalar subtraction of finsets #

                                                                                              def Finset.vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] :
                                                                                              VSub (Finset α) (Finset β)

                                                                                              The pointwise product of two finsets s and t: s -ᵥ t = {x -ᵥ y | x ∈ s, y ∈ t}.

                                                                                              Equations
                                                                                              Instances For
                                                                                                theorem Finset.vsub_def {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t : Finset β} :
                                                                                                s -ᵥ t = Finset.image₂ (fun x x_1 => x -ᵥ x_1) s t
                                                                                                @[simp]
                                                                                                theorem Finset.image_vsub_product {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t : Finset β} :
                                                                                                Finset.image₂ (fun x x_1 => x -ᵥ x_1) s t = s -ᵥ t
                                                                                                theorem Finset.mem_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t : Finset β} {a : α} :
                                                                                                a s -ᵥ t b c, b s c t b -ᵥ c = a
                                                                                                @[simp]
                                                                                                theorem Finset.coe_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] (s : Finset β) (t : Finset β) :
                                                                                                ↑(s -ᵥ t) = s -ᵥ t
                                                                                                theorem Finset.vsub_mem_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t : Finset β} {b : β} {c : β} :
                                                                                                b sc tb -ᵥ c s -ᵥ t
                                                                                                theorem Finset.vsub_card_le {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t : Finset β} :
                                                                                                @[simp]
                                                                                                theorem Finset.empty_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] (t : Finset β) :
                                                                                                @[simp]
                                                                                                theorem Finset.vsub_empty {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] (s : Finset β) :
                                                                                                @[simp]
                                                                                                theorem Finset.vsub_eq_empty {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t : Finset β} :
                                                                                                s -ᵥ t = s = t =
                                                                                                @[simp]
                                                                                                theorem Finset.vsub_nonempty {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t : Finset β} :
                                                                                                theorem Finset.Nonempty.vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t : Finset β} :
                                                                                                theorem Finset.Nonempty.of_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t : Finset β} :
                                                                                                theorem Finset.Nonempty.of_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t : Finset β} :
                                                                                                @[simp]
                                                                                                theorem Finset.vsub_singleton {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} (b : β) :
                                                                                                s -ᵥ {b} = Finset.image (fun x => x -ᵥ b) s
                                                                                                theorem Finset.singleton_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {t : Finset β} (a : β) :
                                                                                                {a} -ᵥ t = Finset.image ((fun x x_1 => x -ᵥ x_1) a) t
                                                                                                theorem Finset.singleton_vsub_singleton {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] (a : β) (b : β) :
                                                                                                {a} -ᵥ {b} = {a -ᵥ b}
                                                                                                theorem Finset.vsub_subset_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s₁ : Finset β} {s₂ : Finset β} {t₁ : Finset β} {t₂ : Finset β} :
                                                                                                s₁ s₂t₁ t₂s₁ -ᵥ t₁ s₂ -ᵥ t₂
                                                                                                theorem Finset.vsub_subset_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t₁ : Finset β} {t₂ : Finset β} :
                                                                                                t₁ t₂s -ᵥ t₁ s -ᵥ t₂
                                                                                                theorem Finset.vsub_subset_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s₁ : Finset β} {s₂ : Finset β} {t : Finset β} :
                                                                                                s₁ s₂s₁ -ᵥ t s₂ -ᵥ t
                                                                                                theorem Finset.vsub_subset_iff {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t : Finset β} {u : Finset α} :
                                                                                                s -ᵥ t u ∀ (x : β), x s∀ (y : β), y tx -ᵥ y u
                                                                                                theorem Finset.union_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s₁ : Finset β} {s₂ : Finset β} {t : Finset β} [DecidableEq β] :
                                                                                                s₁ s₂ -ᵥ t = s₁ -ᵥ t (s₂ -ᵥ t)
                                                                                                theorem Finset.vsub_union {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t₁ : Finset β} {t₂ : Finset β} [DecidableEq β] :
                                                                                                s -ᵥ (t₁ t₂) = s -ᵥ t₁ (s -ᵥ t₂)
                                                                                                theorem Finset.inter_vsub_subset {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s₁ : Finset β} {s₂ : Finset β} {t : Finset β} [DecidableEq β] :
                                                                                                s₁ s₂ -ᵥ t (s₁ -ᵥ t) (s₂ -ᵥ t)
                                                                                                theorem Finset.vsub_inter_subset {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t₁ : Finset β} {t₂ : Finset β} [DecidableEq β] :
                                                                                                s -ᵥ t₁ t₂ (s -ᵥ t₁) (s -ᵥ t₂)
                                                                                                theorem Finset.subset_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {u : Finset α} {s : Set β} {t : Set β} :
                                                                                                u s -ᵥ ts' t', s' s t' t u s' -ᵥ t'

                                                                                                If a finset u is contained in the pointwise subtraction of two sets s -ᵥ t, we can find two finsets s', t' such that s' ⊆ s, t' ⊆ t and u ⊆ s' -ᵥ t'.

                                                                                                Translation/scaling of finsets #

                                                                                                def Finset.vaddFinset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] :
                                                                                                VAdd α (Finset β)

                                                                                                The translation of a finset s by a vector a: a +ᵥ s = {a +ᵥ x | x ∈ s}.

                                                                                                Equations
                                                                                                Instances For
                                                                                                  def Finset.smulFinset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] :
                                                                                                  SMul α (Finset β)

                                                                                                  The scaling of a finset s by a scalar a: a • s = {a • x | x ∈ s}.

                                                                                                  Equations
                                                                                                  • Finset.smulFinset = { smul := fun a => Finset.image ((fun x x_1 => x x_1) a) }
                                                                                                  Instances For
                                                                                                    theorem Finset.vadd_finset_def {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} :
                                                                                                    a +ᵥ s = Finset.image ((fun x x_1 => x +ᵥ x_1) a) s
                                                                                                    theorem Finset.smul_finset_def {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} :
                                                                                                    a s = Finset.image ((fun x x_1 => x x_1) a) s
                                                                                                    theorem Finset.image_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} :
                                                                                                    Finset.image (fun x => a +ᵥ x) s = a +ᵥ s
                                                                                                    theorem Finset.image_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} :
                                                                                                    Finset.image (fun x => a x) s = a s
                                                                                                    theorem Finset.mem_vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} {x : β} :
                                                                                                    x a +ᵥ s y, y s a +ᵥ y = x
                                                                                                    theorem Finset.mem_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} {x : β} :
                                                                                                    x a s y, y s a y = x
                                                                                                    @[simp]
                                                                                                    theorem Finset.coe_vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (a : α) (s : Finset β) :
                                                                                                    ↑(a +ᵥ s) = a +ᵥ s
                                                                                                    @[simp]
                                                                                                    theorem Finset.coe_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (a : α) (s : Finset β) :
                                                                                                    ↑(a s) = a s
                                                                                                    theorem Finset.vadd_mem_vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} {b : β} :
                                                                                                    b sa +ᵥ b a +ᵥ s
                                                                                                    theorem Finset.smul_mem_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} {b : β} :
                                                                                                    b sa b a s
                                                                                                    theorem Finset.vadd_finset_card_le {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} :
                                                                                                    theorem Finset.smul_finset_card_le {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} :
                                                                                                    @[simp]
                                                                                                    theorem Finset.vadd_finset_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (a : α) :
                                                                                                    @[simp]
                                                                                                    theorem Finset.smul_finset_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (a : α) :
                                                                                                    @[simp]
                                                                                                    theorem Finset.vadd_finset_eq_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} :
                                                                                                    a +ᵥ s = s =
                                                                                                    @[simp]
                                                                                                    theorem Finset.smul_finset_eq_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} :
                                                                                                    a s = s =
                                                                                                    @[simp]
                                                                                                    theorem Finset.vadd_finset_nonempty {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} :
                                                                                                    @[simp]
                                                                                                    theorem Finset.smul_finset_nonempty {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} :
                                                                                                    theorem Finset.Nonempty.vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} (hs : Finset.Nonempty s) :
                                                                                                    theorem Finset.Nonempty.smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} (hs : Finset.Nonempty s) :
                                                                                                    @[simp]
                                                                                                    theorem Finset.singleton_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {t : Finset β} (a : α) :
                                                                                                    {a} +ᵥ t = a +ᵥ t
                                                                                                    @[simp]
                                                                                                    theorem Finset.singleton_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {t : Finset β} (a : α) :
                                                                                                    {a} t = a t
                                                                                                    theorem Finset.vadd_finset_subset_vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {t : Finset β} {a : α} :
                                                                                                    s ta +ᵥ s a +ᵥ t
                                                                                                    theorem Finset.smul_finset_subset_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {t : Finset β} {a : α} :
                                                                                                    s ta s a t
                                                                                                    @[simp]
                                                                                                    theorem Finset.vadd_finset_singleton {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {a : α} (b : β) :
                                                                                                    a +ᵥ {b} = {a +ᵥ b}
                                                                                                    @[simp]
                                                                                                    theorem Finset.smul_finset_singleton {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {a : α} (b : β) :
                                                                                                    a {b} = {a b}
                                                                                                    theorem Finset.vadd_finset_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s₁ : Finset β} {s₂ : Finset β} {a : α} :
                                                                                                    a +ᵥ (s₁ s₂) = a +ᵥ s₁ (a +ᵥ s₂)
                                                                                                    theorem Finset.smul_finset_union {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s₁ : Finset β} {s₂ : Finset β} {a : α} :
                                                                                                    a (s₁ s₂) = a s₁ a s₂
                                                                                                    theorem Finset.vadd_finset_inter_subset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s₁ : Finset β} {s₂ : Finset β} {a : α} :
                                                                                                    a +ᵥ s₁ s₂ (a +ᵥ s₁) (a +ᵥ s₂)
                                                                                                    theorem Finset.smul_finset_inter_subset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s₁ : Finset β} {s₂ : Finset β} {a : α} :
                                                                                                    a (s₁ s₂) a s₁ a s₂
                                                                                                    theorem Finset.vadd_finset_subset_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {t : Finset β} {a : α} {s : Finset α} :
                                                                                                    a sa +ᵥ t s +ᵥ t
                                                                                                    theorem Finset.smul_finset_subset_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {t : Finset β} {a : α} {s : Finset α} :
                                                                                                    a sa t s t
                                                                                                    @[simp]
                                                                                                    theorem Finset.biUnion_vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (s : Finset α) (t : Finset β) :
                                                                                                    (Finset.biUnion s fun x => x +ᵥ t) = s +ᵥ t
                                                                                                    @[simp]
                                                                                                    theorem Finset.biUnion_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (s : Finset α) (t : Finset β) :
                                                                                                    (Finset.biUnion s fun x => x t) = s t
                                                                                                    theorem Finset.vaddCommClass_finset.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
                                                                                                    theorem Finset.vaddCommClass_finset'.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
                                                                                                    theorem Finset.vaddCommClass_finset''.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
                                                                                                    instance Finset.vaddCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
                                                                                                    Equations
                                                                                                    theorem Finset.vaddCommClass.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
                                                                                                    instance Finset.smulCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
                                                                                                    Equations
                                                                                                    theorem Finset.vaddAssocClass.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq γ] [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :
                                                                                                    instance Finset.vaddAssocClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :
                                                                                                    Equations
                                                                                                    instance Finset.isScalarTower {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
                                                                                                    Equations
                                                                                                    theorem Finset.vaddAssocClass'.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq γ] [DecidableEq β] [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :
                                                                                                    instance Finset.vaddAssocClass' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [DecidableEq β] [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :
                                                                                                    Equations
                                                                                                    instance Finset.isScalarTower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [DecidableEq β] [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
                                                                                                    Equations
                                                                                                    theorem Finset.vaddAssocClass''.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq γ] [DecidableEq β] [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :
                                                                                                    instance Finset.vaddAssocClass'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [DecidableEq β] [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :
                                                                                                    Equations
                                                                                                    instance Finset.isScalarTower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [DecidableEq β] [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
                                                                                                    Equations
                                                                                                    theorem Finset.isCentralVAdd.proof_1 {α : Type u_1} {β : Type u_2} [DecidableEq β] [VAdd α β] [VAdd αᵃᵒᵖ β] [IsCentralVAdd α β] :
                                                                                                    def Finset.addAction {α : Type u_2} {β : Type u_3} [DecidableEq β] [DecidableEq α] [AddMonoid α] [AddAction α β] :

                                                                                                    An additive action of an additive monoid α on a type β gives an additive action of Finset α on Finset β

                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For
                                                                                                      theorem Finset.addAction.proof_1 {α : Type u_2} {β : Type u_1} [DecidableEq β] [AddMonoid α] [AddAction α β] (s : Finset β) :
                                                                                                      Finset.image₂ (fun x x_1 => x +ᵥ x_1) {0} s = s
                                                                                                      theorem Finset.addAction.proof_2 {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] [AddMonoid α] [AddAction α β] :
                                                                                                      ∀ (x x_1 : Finset α) (x_2 : Finset β), Finset.image₂ (fun x x_3 => x +ᵥ x_3) (Finset.image₂ (fun x x_3 => x + x_3) x x_1) x_2 = Finset.image₂ (fun x x_3 => x +ᵥ x_3) x (Finset.image₂ (fun x x_3 => x +ᵥ x_3) x_1 x_2)
                                                                                                      def Finset.mulAction {α : Type u_2} {β : Type u_3} [DecidableEq β] [DecidableEq α] [Monoid α] [MulAction α β] :

                                                                                                      A multiplicative action of a monoid α on a type β gives a multiplicative action of Finset α on Finset β.

                                                                                                      Equations
                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                      Instances For
                                                                                                        def Finset.addActionFinset {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddMonoid α] [AddAction α β] :

                                                                                                        An additive action of an additive monoid on a type β gives an additive action on Finset β.

                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          theorem Finset.addActionFinset.proof_1 {α : Type u_2} {β : Type u_1} [DecidableEq β] [AddMonoid α] [AddAction α β] (a : α) (s : Finset β) :
                                                                                                          ↑(a +ᵥ s) = a +ᵥ s
                                                                                                          def Finset.mulActionFinset {α : Type u_2} {β : Type u_3} [DecidableEq β] [Monoid α] [MulAction α β] :

                                                                                                          A multiplicative action of a monoid on a type β gives a multiplicative action on Finset β.

                                                                                                          Equations
                                                                                                          Instances For

                                                                                                            A distributive multiplicative action of a monoid on an additive monoid β gives a distributive multiplicative action on Finset β.

                                                                                                            Equations
                                                                                                            Instances For

                                                                                                              A multiplicative action of a monoid on a monoid β gives a multiplicative action on Set β.

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                theorem Finset.op_vadd_finset_vadd_eq_vadd_vadd_finset {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq β] [DecidableEq γ] [VAdd αᵃᵒᵖ β] [VAdd β γ] [VAdd α γ] (a : α) (s : Finset β) (t : Finset γ) (h : ∀ (a : α) (b : β) (c : γ), AddOpposite.op a +ᵥ b +ᵥ c = b +ᵥ (a +ᵥ c)) :
                                                                                                                theorem Finset.op_smul_finset_smul_eq_smul_smul_finset {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq β] [DecidableEq γ] [SMul αᵐᵒᵖ β] [SMul β γ] [SMul α γ] (a : α) (s : Finset β) (t : Finset γ) (h : ∀ (a : α) (b : β) (c : γ), (MulOpposite.op a b) c = b a c) :
                                                                                                                (MulOpposite.op a s) t = s a t
                                                                                                                theorem Finset.op_vadd_finset_subset_add {α : Type u_2} [Add α] [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} :
                                                                                                                a tAddOpposite.op a +ᵥ s s + t
                                                                                                                theorem Finset.op_smul_finset_subset_mul {α : Type u_2} [Mul α] [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} :
                                                                                                                a tMulOpposite.op a s s * t
                                                                                                                @[simp]
                                                                                                                theorem Finset.biUnion_op_vadd_finset {α : Type u_2} [Add α] [DecidableEq α] (s : Finset α) (t : Finset α) :
                                                                                                                (Finset.biUnion t fun a => AddOpposite.op a +ᵥ s) = s + t
                                                                                                                @[simp]
                                                                                                                theorem Finset.biUnion_op_smul_finset {α : Type u_2} [Mul α] [DecidableEq α] (s : Finset α) (t : Finset α) :
                                                                                                                (Finset.biUnion t fun a => MulOpposite.op a s) = s * t
                                                                                                                theorem Finset.add_subset_iff_left {α : Type u_2} [Add α] [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} :
                                                                                                                s + t u ∀ (a : α), a sa +ᵥ t u
                                                                                                                theorem Finset.mul_subset_iff_left {α : Type u_2} [Mul α] [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} :
                                                                                                                s * t u ∀ (a : α), a sa t u
                                                                                                                theorem Finset.add_subset_iff_right {α : Type u_2} [Add α] [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} :
                                                                                                                s + t u ∀ (b : α), b tAddOpposite.op b +ᵥ s u
                                                                                                                theorem Finset.mul_subset_iff_right {α : Type u_2} [Mul α] [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} :
                                                                                                                s * t u ∀ (b : α), b tMulOpposite.op b s u
                                                                                                                theorem Finset.op_vadd_finset_add_eq_add_vadd_finset {α : Type u_2} [AddSemigroup α] [DecidableEq α] (a : α) (s : Finset α) (t : Finset α) :
                                                                                                                AddOpposite.op a +ᵥ s + t = s + (a +ᵥ t)
                                                                                                                theorem Finset.op_smul_finset_mul_eq_mul_smul_finset {α : Type u_2} [Semigroup α] [DecidableEq α] (a : α) (s : Finset α) (t : Finset α) :
                                                                                                                MulOpposite.op a s * t = s * a t
                                                                                                                theorem Finset.pairwiseDisjoint_vadd_iff {α : Type u_2} [AddLeftCancelSemigroup α] [DecidableEq α] {s : Set α} {t : Finset α} :
                                                                                                                (Set.PairwiseDisjoint s fun x => x +ᵥ t) Set.InjOn (fun p => p.fst + p.snd) (s ×ˢ t)
                                                                                                                theorem Finset.pairwiseDisjoint_smul_iff {α : Type u_2} [LeftCancelSemigroup α] [DecidableEq α] {s : Set α} {t : Finset α} :
                                                                                                                (Set.PairwiseDisjoint s fun x => x t) Set.InjOn (fun p => p.fst * p.snd) (s ×ˢ t)
                                                                                                                @[simp]
                                                                                                                theorem Finset.card_singleton_add {α : Type u_2} [AddLeftCancelSemigroup α] [DecidableEq α] (t : Finset α) (a : α) :
                                                                                                                @[simp]
                                                                                                                theorem Finset.card_singleton_mul {α : Type u_2} [LeftCancelSemigroup α] [DecidableEq α] (t : Finset α) (a : α) :
                                                                                                                theorem Finset.singleton_add_inter {α : Type u_2} [AddLeftCancelSemigroup α] [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) :
                                                                                                                {a} + s t = ({a} + s) ({a} + t)
                                                                                                                theorem Finset.singleton_mul_inter {α : Type u_2} [LeftCancelSemigroup α] [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) :
                                                                                                                {a} * (s t) = {a} * s ({a} * t)
                                                                                                                @[simp]
                                                                                                                theorem Finset.card_add_singleton {α : Type u_2} [AddRightCancelSemigroup α] [DecidableEq α] (s : Finset α) (a : α) :
                                                                                                                @[simp]
                                                                                                                theorem Finset.card_mul_singleton {α : Type u_2} [RightCancelSemigroup α] [DecidableEq α] (s : Finset α) (a : α) :
                                                                                                                theorem Finset.inter_add_singleton {α : Type u_2} [AddRightCancelSemigroup α] [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) :
                                                                                                                s t + {a} = (s + {a}) (t + {a})
                                                                                                                theorem Finset.inter_mul_singleton {α : Type u_2} [RightCancelSemigroup α] [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) :
                                                                                                                s t * {a} = s * {a} (t * {a})
                                                                                                                theorem Finset.image_vadd_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq β] [DecidableEq γ] [VAdd α β] [VAdd α γ] (f : βγ) (a : α) (s : Finset β) :
                                                                                                                (∀ (b : β), f (a +ᵥ b) = a +ᵥ f b) → Finset.image f (a +ᵥ s) = a +ᵥ Finset.image f s
                                                                                                                theorem Finset.image_smul_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq β] [DecidableEq γ] [SMul α β] [SMul α γ] (f : βγ) (a : α) (s : Finset β) :
                                                                                                                (∀ (b : β), f (a b) = a f b) → Finset.image f (a s) = a Finset.image f s
                                                                                                                theorem Finset.image_vadd_distrib {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [AddMonoid α] [AddMonoid β] [AddMonoidHomClass F α β] (f : F) (a : α) (s : Finset α) :
                                                                                                                Finset.image (f) (a +ᵥ s) = f a +ᵥ Finset.image (f) s
                                                                                                                theorem Finset.image_smul_distrib {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Monoid α] [Monoid β] [MonoidHomClass F α β] (f : F) (a : α) (s : Finset α) :
                                                                                                                Finset.image (f) (a s) = f a Finset.image (f) s
                                                                                                                @[simp]
                                                                                                                theorem Finset.vadd_mem_vadd_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {b : β} (a : α) :
                                                                                                                a +ᵥ b a +ᵥ s b s
                                                                                                                @[simp]
                                                                                                                theorem Finset.smul_mem_smul_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {b : β} (a : α) :
                                                                                                                a b a s b s
                                                                                                                theorem Finset.neg_vadd_mem_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {a : α} {b : β} :
                                                                                                                -a +ᵥ b s b a +ᵥ s
                                                                                                                theorem Finset.inv_smul_mem_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {a : α} {b : β} :
                                                                                                                a⁻¹ b s b a s
                                                                                                                theorem Finset.mem_neg_vadd_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {a : α} {b : β} :
                                                                                                                b -a +ᵥ s a +ᵥ b s
                                                                                                                theorem Finset.mem_inv_smul_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {a : α} {b : β} :
                                                                                                                b a⁻¹ s a b s
                                                                                                                @[simp]
                                                                                                                theorem Finset.vadd_finset_subset_vadd_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {t : Finset β} {a : α} :
                                                                                                                a +ᵥ s a +ᵥ t s t
                                                                                                                @[simp]
                                                                                                                theorem Finset.smul_finset_subset_smul_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} :
                                                                                                                a s a t s t
                                                                                                                theorem Finset.vadd_finset_subset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {t : Finset β} {a : α} :
                                                                                                                a +ᵥ s t s -a +ᵥ t
                                                                                                                theorem Finset.smul_finset_subset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} :
                                                                                                                a s t s a⁻¹ t
                                                                                                                theorem Finset.subset_vadd_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {t : Finset β} {a : α} :
                                                                                                                s a +ᵥ t -a +ᵥ s t
                                                                                                                theorem Finset.subset_smul_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} :
                                                                                                                s a t a⁻¹ s t
                                                                                                                theorem Finset.vadd_finset_inter {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {t : Finset β} {a : α} :
                                                                                                                a +ᵥ s t = (a +ᵥ s) (a +ᵥ t)
                                                                                                                theorem Finset.smul_finset_inter {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} :
                                                                                                                a (s t) = a s a t
                                                                                                                theorem Finset.vadd_finset_sdiff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {t : Finset β} {a : α} :
                                                                                                                a +ᵥ s \ t = (a +ᵥ s) \ (a +ᵥ t)
                                                                                                                theorem Finset.smul_finset_sdiff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} :
                                                                                                                a (s \ t) = a s \ a t
                                                                                                                theorem Finset.vadd_finset_symmDiff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {t : Finset β} {a : α} :
                                                                                                                a +ᵥ s t = (a +ᵥ s) (a +ᵥ t)
                                                                                                                theorem Finset.smul_finset_symmDiff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} :
                                                                                                                a s t = (a s) (a t)
                                                                                                                @[simp]
                                                                                                                theorem Finset.vadd_finset_univ {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {a : α} [Fintype β] :
                                                                                                                a +ᵥ Finset.univ = Finset.univ
                                                                                                                @[simp]
                                                                                                                theorem Finset.smul_finset_univ {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {a : α} [Fintype β] :
                                                                                                                a Finset.univ = Finset.univ
                                                                                                                @[simp]
                                                                                                                theorem Finset.vadd_univ {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] [Fintype β] {s : Finset α} (hs : Finset.Nonempty s) :
                                                                                                                s +ᵥ Finset.univ = Finset.univ
                                                                                                                @[simp]
                                                                                                                theorem Finset.smul_univ {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] [Fintype β] {s : Finset α} (hs : Finset.Nonempty s) :
                                                                                                                s Finset.univ = Finset.univ
                                                                                                                @[simp]
                                                                                                                theorem Finset.card_vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] (a : α) (s : Finset β) :
                                                                                                                @[simp]
                                                                                                                theorem Finset.card_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] (a : α) (s : Finset β) :
                                                                                                                theorem Finset.card_dvd_card_vadd_right {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {t : Finset β} {s : Finset α} :
                                                                                                                Set.PairwiseDisjoint ((fun x => x +ᵥ t) '' s) idFinset.card t Finset.card (s +ᵥ t)

                                                                                                                If the left cosets of t by elements of s are disjoint (but not necessarily distinct!), then the size of t divides the size of s +ᵥ t.

                                                                                                                theorem Finset.card_dvd_card_smul_right {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {t : Finset β} {s : Finset α} :
                                                                                                                Set.PairwiseDisjoint ((fun x => x t) '' s) idFinset.card t Finset.card (s t)

                                                                                                                If the left cosets of t by elements of s are disjoint (but not necessarily distinct!), then the size of t divides the size of s • t.

                                                                                                                theorem Finset.card_dvd_card_add_left {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} {t : Finset α} :
                                                                                                                Set.PairwiseDisjoint ((fun b => Finset.image (fun a => a + b) s) '' t) idFinset.card s Finset.card (s + t)

                                                                                                                If the right cosets of s by elements of t are disjoint (but not necessarily distinct!), then the size of s divides the size of s + t.

                                                                                                                theorem Finset.card_dvd_card_mul_left {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} {t : Finset α} :
                                                                                                                Set.PairwiseDisjoint ((fun b => Finset.image (fun a => a * b) s) '' t) idFinset.card s Finset.card (s * t)

                                                                                                                If the right cosets of s by elements of t are disjoint (but not necessarily distinct!), then the size of s divides the size of s * t.

                                                                                                                theorem Finset.card_dvd_card_add_right {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} {t : Finset α} :
                                                                                                                Set.PairwiseDisjoint ((fun x => x +ᵥ t) '' s) idFinset.card t Finset.card (s + t)

                                                                                                                If the left cosets of t by elements of s are disjoint (but not necessarily distinct!), then the size of t divides the size of s + t.

                                                                                                                theorem Finset.card_dvd_card_mul_right {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} {t : Finset α} :
                                                                                                                Set.PairwiseDisjoint ((fun x => x t) '' s) idFinset.card t Finset.card (s * t)

                                                                                                                If the left cosets of t by elements of s are disjoint (but not necessarily distinct!), then the size of t divides the size of s * t.

                                                                                                                @[simp]
                                                                                                                theorem Finset.smul_mem_smul_finset_iff₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {s : Finset β} {a : α} {b : β} (ha : a 0) :
                                                                                                                a b a s b s
                                                                                                                theorem Finset.inv_smul_mem_iff₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {s : Finset β} {a : α} {b : β} (ha : a 0) :
                                                                                                                a⁻¹ b s b a s
                                                                                                                theorem Finset.mem_inv_smul_finset_iff₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {s : Finset β} {a : α} {b : β} (ha : a 0) :
                                                                                                                b a⁻¹ s a b s
                                                                                                                @[simp]
                                                                                                                theorem Finset.smul_finset_subset_smul_finset_iff₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} (ha : a 0) :
                                                                                                                a s a t s t
                                                                                                                theorem Finset.smul_finset_subset_iff₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} (ha : a 0) :
                                                                                                                a s t s a⁻¹ t
                                                                                                                theorem Finset.subset_smul_finset_iff₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} (ha : a 0) :
                                                                                                                s a t a⁻¹ s t
                                                                                                                theorem Finset.smul_finset_inter₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} (ha : a 0) :
                                                                                                                a (s t) = a s a t
                                                                                                                theorem Finset.smul_finset_sdiff₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} (ha : a 0) :
                                                                                                                a (s \ t) = a s \ a t
                                                                                                                theorem Finset.smul_finset_symmDiff₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} (ha : a 0) :
                                                                                                                a s t = (a s) (a t)
                                                                                                                theorem Finset.smul_univ₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] [Fintype β] {s : Finset α} (hs : ¬s 0) :
                                                                                                                s Finset.univ = Finset.univ
                                                                                                                theorem Finset.smul_finset_univ₀ {α : Type u_2} {β : Type u_3} [DecidableEq β] [GroupWithZero α] [MulAction α β] {a : α} [Fintype β] (ha : a 0) :
                                                                                                                a Finset.univ = Finset.univ

                                                                                                                Note that we have neither SMulWithZero α (Finset β) nor SMulWithZero (Finset α) (Finset β) because 0 * ∅ ≠ 0.

                                                                                                                theorem Finset.smul_zero_subset {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] [DecidableEq β] (s : Finset α) :
                                                                                                                s 0 0
                                                                                                                theorem Finset.zero_smul_subset {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] [DecidableEq β] (t : Finset β) :
                                                                                                                0 t 0
                                                                                                                theorem Finset.Nonempty.smul_zero {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] [DecidableEq β] {s : Finset α} (hs : Finset.Nonempty s) :
                                                                                                                s 0 = 0
                                                                                                                theorem Finset.Nonempty.zero_smul {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] [DecidableEq β] {t : Finset β} (ht : Finset.Nonempty t) :
                                                                                                                0 t = 0
                                                                                                                theorem Finset.zero_smul_finset {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] [DecidableEq β] {s : Finset β} (h : Finset.Nonempty s) :
                                                                                                                0 s = 0

                                                                                                                A nonempty set is scaled by zero to the singleton set containing 0.

                                                                                                                theorem Finset.zero_smul_finset_subset {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] [DecidableEq β] (s : Finset β) :
                                                                                                                0 s 0
                                                                                                                theorem Finset.zero_mem_smul_finset {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] [DecidableEq β] {t : Finset β} {a : α} (h : 0 t) :
                                                                                                                0 a t
                                                                                                                theorem Finset.zero_mem_smul_iff {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] [DecidableEq β] {s : Finset α} {t : Finset β} [NoZeroSMulDivisors α β] :
                                                                                                                theorem Finset.zero_mem_smul_finset_iff {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] [DecidableEq β] {t : Finset β} [NoZeroSMulDivisors α β] {a : α} (ha : a 0) :
                                                                                                                0 a t 0 t
                                                                                                                @[simp]
                                                                                                                theorem Finset.smul_finset_neg {α : Type u_2} {β : Type u_3} [Monoid α] [AddGroup β] [DistribMulAction α β] [DecidableEq β] (a : α) (t : Finset β) :
                                                                                                                a -t = -(a t)
                                                                                                                @[simp]
                                                                                                                theorem Finset.smul_neg {α : Type u_2} {β : Type u_3} [Monoid α] [AddGroup β] [DistribMulAction α β] [DecidableEq β] (s : Finset α) (t : Finset β) :
                                                                                                                s -t = -(s t)
                                                                                                                @[simp]
                                                                                                                theorem Finset.neg_smul_finset {α : Type u_2} {β : Type u_3} [Ring α] [AddCommGroup β] [Module α β] [DecidableEq β] {t : Finset β} {a : α} :
                                                                                                                -a t = -(a t)
                                                                                                                @[simp]
                                                                                                                theorem Finset.neg_smul {α : Type u_2} {β : Type u_3} [Ring α] [AddCommGroup β] [Module α β] [DecidableEq β] {s : Finset α} {t : Finset β} [DecidableEq α] :
                                                                                                                -s t = -(s t)
                                                                                                                @[simp]
                                                                                                                theorem Set.toFinset_zero {α : Type u_2} [Zero α] :
                                                                                                                @[simp]
                                                                                                                theorem Set.toFinset_one {α : Type u_2} [One α] :
                                                                                                                @[simp]
                                                                                                                theorem Set.Finite.toFinset_zero {α : Type u_2} [Zero α] (h : optParam (Set.Finite 0) (_ : Set.Finite 0)) :
                                                                                                                @[simp]
                                                                                                                theorem Set.Finite.toFinset_one {α : Type u_2} [One α] (h : optParam (Set.Finite 1) (_ : Set.Finite 1)) :
                                                                                                                @[simp]
                                                                                                                theorem Set.toFinset_add {α : Type u_2} [DecidableEq α] [Add α] (s : Set α) (t : Set α) [Fintype s] [Fintype t] [Fintype ↑(s + t)] :
                                                                                                                @[simp]
                                                                                                                theorem Set.toFinset_mul {α : Type u_2} [DecidableEq α] [Mul α] (s : Set α) (t : Set α) [Fintype s] [Fintype t] [Fintype ↑(s * t)] :
                                                                                                                theorem Set.Finite.toFinset_add {α : Type u_2} [DecidableEq α] [Add α] {s : Set α} {t : Set α} (hs : Set.Finite s) (ht : Set.Finite t) (hf : optParam (Set.Finite (s + t)) (_ : Set.Finite (s + t))) :
                                                                                                                theorem Set.Finite.toFinset_mul {α : Type u_2} [DecidableEq α] [Mul α] {s : Set α} {t : Set α} (hs : Set.Finite s) (ht : Set.Finite t) (hf : optParam (Set.Finite (s * t)) (_ : Set.Finite (s * t))) :
                                                                                                                @[simp]
                                                                                                                theorem Set.toFinset_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] [DecidableEq β] (s : Set α) (t : Set β) [Fintype s] [Fintype t] [Fintype ↑(s +ᵥ t)] :
                                                                                                                @[simp]
                                                                                                                theorem Set.toFinset_smul {α : Type u_2} {β : Type u_3} [SMul α β] [DecidableEq β] (s : Set α) (t : Set β) [Fintype s] [Fintype t] [Fintype ↑(s t)] :
                                                                                                                theorem Set.Finite.toFinset_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] [DecidableEq β] {s : Set α} {t : Set β} (hs : Set.Finite s) (ht : Set.Finite t) (hf : optParam (Set.Finite (s +ᵥ t)) (_ : Set.Finite (s +ᵥ t))) :
                                                                                                                theorem Set.Finite.toFinset_smul {α : Type u_2} {β : Type u_3} [SMul α β] [DecidableEq β] {s : Set α} {t : Set β} (hs : Set.Finite s) (ht : Set.Finite t) (hf : optParam (Set.Finite (s t)) (_ : Set.Finite (s t))) :
                                                                                                                @[simp]
                                                                                                                theorem Set.toFinset_vadd_set {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (a : α) (s : Set β) [Fintype s] [Fintype ↑(a +ᵥ s)] :
                                                                                                                @[simp]
                                                                                                                theorem Set.toFinset_smul_set {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (a : α) (s : Set β) [Fintype s] [Fintype ↑(a s)] :
                                                                                                                theorem Set.Finite.toFinset_vadd_set {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {a : α} {s : Set β} (hs : Set.Finite s) (hf : optParam (Set.Finite (a +ᵥ s)) (_ : Set.Finite (a +ᵥ s))) :
                                                                                                                theorem Set.Finite.toFinset_smul_set {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {a : α} {s : Set β} (hs : Set.Finite s) (hf : optParam (Set.Finite (a s)) (_ : Set.Finite (a s))) :
                                                                                                                @[simp]
                                                                                                                theorem Set.toFinset_vsub {α : Type u_2} {β : Type u_3} [DecidableEq α] [VSub α β] (s : Set β) (t : Set β) [Fintype s] [Fintype t] [Fintype ↑(s -ᵥ t)] :
                                                                                                                theorem Set.Finite.toFinset_vsub {α : Type u_2} {β : Type u_3} [DecidableEq α] [VSub α β] {s : Set β} {t : Set β} (hs : Set.Finite s) (ht : Set.Finite t) (hf : optParam (Set.Finite (s -ᵥ t)) (_ : Set.Finite (s -ᵥ t))) :