# Pointwise operations of finsets #

This file defines pointwise algebraic operations on finsets.

## Main declarations #

For finsets s and t:

• 0 (Finset.zero): The singleton {0}.
• 1 (Finset.one): The singleton {1}.
• -s (Finset.neg): Negation, finset of all -x where x ∈ s.
• s⁻¹ (Finset.inv): Inversion, finset of all x⁻¹ where x ∈ s.
• s + t (Finset.add): Addition, finset of all x + y where x ∈ s and y ∈ t.
• s * t (Finset.mul): Multiplication, finset of all x * y where x ∈ s and y ∈ t.
• s - t (Finset.sub): Subtraction, finset of all x - y where x ∈ s and y ∈ t.
• s / t (Finset.div): Division, finset of all x / y where x ∈ s and y ∈ t.
• s +ᵥ t (Finset.vadd): Scalar addition, finset of all x +ᵥ y where x ∈ s and y ∈ t.
• s • t (Finset.smul): Scalar multiplication, finset of all x • y where x ∈ s and y ∈ t.
• s -ᵥ t (Finset.vsub): Scalar subtraction, finset of all x -ᵥ y where x ∈ s and y ∈ t.
• a • s (Finset.smulFinset): Scaling, finset of all a • x where x ∈ s.
• a +ᵥ s (Finset.vaddFinset): Translation, finset of all a +ᵥ x where x ∈ s.

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 #

### 0/1 as finsets #

def Finset.zero {α : Type u_2} [Zero α] :
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 ()

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.coe_eq_zero {α : Type u_2} [Zero α] {s : } :
s = 0 s = 0
@[simp]
theorem Finset.coe_eq_one {α : Type u_2} [One α] {s : } :
s = 1 s = 1
@[simp]
theorem Finset.zero_subset {α : Type u_2} [Zero α] {s : } :
0 s 0 s
@[simp]
theorem Finset.one_subset {α : Type u_2} [One α] {s : } :
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.zero_nonempty {α : Type u_2} [Zero α] :
0.Nonempty
@[simp]
theorem Finset.one_nonempty {α : Type u_2} [One α] :
1.Nonempty
@[simp]
theorem Finset.map_zero {α : Type u_2} {β : Type u_3} [Zero α] {f : α β} :
= {f 0}
@[simp]
theorem Finset.map_one {α : Type u_2} {β : Type u_3} [One α] {f : α β} :
= {f 1}
@[simp]
theorem Finset.image_zero {α : Type u_2} {β : Type u_3} [Zero α] [] {f : αβ} :
= {f 0}
@[simp]
theorem Finset.image_one {α : Type u_2} {β : Type u_3} [One α] [] {f : αβ} :
= {f 1}
theorem Finset.subset_zero_iff_eq {α : Type u_2} [Zero α] {s : } :
s 0 s = s = 0
theorem Finset.subset_one_iff_eq {α : Type u_2} [One α] {s : } :
s 1 s = s = 1
theorem Finset.Nonempty.subset_zero_iff {α : Type u_2} [Zero α] {s : } (h : s.Nonempty) :
s 0 s = 0
theorem Finset.Nonempty.subset_one_iff {α : Type u_2} [One α] {s : } (h : s.Nonempty) :
s 1 s = 1
@[simp]
theorem Finset.card_zero {α : Type u_2} [Zero α] :
0.card = 1
@[simp]
theorem Finset.card_one {α : Type u_2} [One α] :
1.card = 1
def Finset.singletonZeroHom {α : Type u_2} [Zero α] :
ZeroHom α ()

The singleton operation as a ZeroHom.

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

The singleton operation as a OneHom.

Equations
• Finset.singletonOneHom = { toFun := singleton, map_one' := }
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}
def Finset.imageZeroHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Zero α] [] [Zero β] [FunLike F α β] [ZeroHomClass F α β] (f : F) :
ZeroHom () ()

Lift a ZeroHom to Finset via image

Equations
• = { toFun := , map_zero' := }
Instances For
theorem Finset.imageZeroHom.proof_1 {F : Type u_3} {α : Type u_2} {β : Type u_1} [Zero α] [] [Zero β] [FunLike F α β] [ZeroHomClass F α β] (f : F) :
Finset.image (f) 0 = 0
@[simp]
theorem Finset.imageOneHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [One α] [] [One β] [FunLike F α β] [OneHomClass F α β] (f : F) (s : ) :
s = Finset.image (f) s
@[simp]
theorem Finset.imageZeroHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [Zero α] [] [Zero β] [FunLike F α β] [ZeroHomClass F α β] (f : F) (s : ) :
s = Finset.image (f) s
def Finset.imageOneHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [One α] [] [One β] [FunLike F α β] [OneHomClass F α β] (f : F) :
OneHom () ()

Lift a OneHom to Finset via image.

Equations
• = { toFun := , map_one' := }
Instances For
@[simp]
theorem Finset.sup_zero {α : Type u_2} {β : Type u_3} [Zero α] [] [] (f : αβ) :
= f 0
@[simp]
theorem Finset.sup_one {α : Type u_2} {β : Type u_3} [One α] [] [] (f : αβ) :
= f 1
@[simp]
theorem Finset.sup'_zero {α : Type u_2} {β : Type u_3} [Zero α] [] (f : αβ) :
Finset.sup' 0 f = f 0
@[simp]
theorem Finset.sup'_one {α : Type u_2} {β : Type u_3} [One α] [] (f : αβ) :
Finset.sup' 1 f = f 1
@[simp]
theorem Finset.inf_zero {α : Type u_2} {β : Type u_3} [Zero α] [] [] (f : αβ) :
= f 0
@[simp]
theorem Finset.inf_one {α : Type u_2} {β : Type u_3} [One α] [] [] (f : αβ) :
= f 1
@[simp]
theorem Finset.inf'_zero {α : Type u_2} {β : Type u_3} [Zero α] [] (f : αβ) :
Finset.inf' 0 f = f 0
@[simp]
theorem Finset.inf'_one {α : Type u_2} {β : Type u_3} [One α] [] (f : αβ) :
Finset.inf' 1 f = f 1
@[simp]
theorem Finset.max_zero {α : Type u_2} [Zero α] [] :
= 0
@[simp]
theorem Finset.max_one {α : Type u_2} [One α] [] :
= 1
@[simp]
theorem Finset.min_zero {α : Type u_2} [Zero α] [] :
= 0
@[simp]
theorem Finset.min_one {α : Type u_2} [One α] [] :
= 1
@[simp]
theorem Finset.max'_zero {α : Type u_2} [Zero α] [] :
= 0
@[simp]
theorem Finset.max'_one {α : Type u_2} [One α] [] :
= 1
@[simp]
theorem Finset.min'_zero {α : Type u_2} [Zero α] [] :
= 0
@[simp]
theorem Finset.min'_one {α : Type u_2} [One α] [] :
= 1

### Finset negation/inversion #

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

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

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

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} [] [Neg α] {s : } :
-s = Finset.image (fun (x : α) => -x) s
theorem Finset.inv_def {α : Type u_2} [] [Inv α] {s : } :
s⁻¹ = Finset.image (fun (x : α) => x⁻¹) s
theorem Finset.image_neg {α : Type u_2} [] [Neg α] {s : } :
Finset.image (fun (x : α) => -x) s = -s
theorem Finset.image_inv {α : Type u_2} [] [Inv α] {s : } :
Finset.image (fun (x : α) => x⁻¹) s = s⁻¹
theorem Finset.mem_neg {α : Type u_2} [] [Neg α] {s : } {x : α} :
x -s ∃ y ∈ s, -y = x
theorem Finset.mem_inv {α : Type u_2} [] [Inv α] {s : } {x : α} :
x s⁻¹ ∃ y ∈ s, y⁻¹ = x
theorem Finset.neg_mem_neg {α : Type u_2} [] [Neg α] {s : } {a : α} (ha : a s) :
-a -s
theorem Finset.inv_mem_inv {α : Type u_2} [] [Inv α] {s : } {a : α} (ha : a s) :
theorem Finset.card_neg_le {α : Type u_2} [] [Neg α] {s : } :
(-s).card s.card
theorem Finset.card_inv_le {α : Type u_2} [] [Inv α] {s : } :
s⁻¹.card s.card
@[simp]
theorem Finset.neg_empty {α : Type u_2} [] [Neg α] :
@[simp]
theorem Finset.inv_empty {α : Type u_2} [] [Inv α] :
@[simp]
theorem Finset.neg_nonempty_iff {α : Type u_2} [] [Neg α] {s : } :
(-s).Nonempty s.Nonempty
@[simp]
theorem Finset.inv_nonempty_iff {α : Type u_2} [] [Inv α] {s : } :
s⁻¹.Nonempty s.Nonempty
theorem Finset.Nonempty.of_inv {α : Type u_2} [] [Inv α] {s : } :
s⁻¹.Nonemptys.Nonempty

Alias of the forward direction of Finset.inv_nonempty_iff.

theorem Finset.Nonempty.inv {α : Type u_2} [] [Inv α] {s : } :
s.Nonemptys⁻¹.Nonempty

Alias of the reverse direction of Finset.inv_nonempty_iff.

theorem Finset.Nonempty.of_neg {α : Type u_2} [] [Neg α] {s : } :
(-s).Nonemptys.Nonempty
theorem Finset.Nonempty.neg {α : Type u_2} [] [Neg α] {s : } :
s.Nonempty(-s).Nonempty
@[simp]
theorem Finset.neg_eq_empty {α : Type u_2} [] [Neg α] {s : } :
-s = s =
@[simp]
theorem Finset.inv_eq_empty {α : Type u_2} [] [Inv α] {s : } :
theorem Finset.neg_subset_neg {α : Type u_2} [] [Neg α] {s : } {t : } (h : s t) :
-s -t
theorem Finset.inv_subset_inv {α : Type u_2} [] [Inv α] {s : } {t : } (h : s t) :
@[simp]
theorem Finset.neg_singleton {α : Type u_2} [] [Neg α] (a : α) :
-{a} = {-a}
@[simp]
theorem Finset.inv_singleton {α : Type u_2} [] [Inv α] (a : α) :
{a}⁻¹ = {a⁻¹}
@[simp]
theorem Finset.neg_insert {α : Type u_2} [] [Neg α] (a : α) (s : ) :
-insert a s = insert (-a) (-s)
@[simp]
theorem Finset.inv_insert {α : Type u_2} [] [Inv α] (a : α) (s : ) :
(insert a s)⁻¹ =
@[simp]
theorem Finset.sup_neg {α : Type u_2} {β : Type u_3} [] [Neg α] [] [] (s : ) (f : αβ) :
Finset.sup (-s) f = Finset.sup s fun (x : α) => f (-x)
@[simp]
theorem Finset.sup_inv {α : Type u_2} {β : Type u_3} [] [Inv α] [] [] (s : ) (f : αβ) :
= Finset.sup s fun (x : α) => f x⁻¹
@[simp]
theorem Finset.sup'_neg {α : Type u_2} {β : Type u_3} [] [Neg α] [] {s : } (hs : (-s).Nonempty) (f : αβ) :
Finset.sup' (-s) hs f = Finset.sup' s fun (x : α) => f (-x)
@[simp]
theorem Finset.sup'_inv {α : Type u_2} {β : Type u_3} [] [Inv α] [] {s : } (hs : s⁻¹.Nonempty) (f : αβ) :
Finset.sup' s⁻¹ hs f = Finset.sup' s fun (x : α) => f x⁻¹
@[simp]
theorem Finset.inf_neg {α : Type u_2} {β : Type u_3} [] [Neg α] [] [] (s : ) (f : αβ) :
Finset.inf (-s) f = Finset.inf s fun (x : α) => f (-x)
@[simp]
theorem Finset.inf_inv {α : Type u_2} {β : Type u_3} [] [Inv α] [] [] (s : ) (f : αβ) :
= Finset.inf s fun (x : α) => f x⁻¹
@[simp]
theorem Finset.inf'_neg {α : Type u_2} {β : Type u_3} [] [Neg α] [] {s : } (hs : (-s).Nonempty) (f : αβ) :
Finset.inf' (-s) hs f = Finset.inf' s fun (x : α) => f (-x)
@[simp]
theorem Finset.inf'_inv {α : Type u_2} {β : Type u_3} [] [Inv α] [] {s : } (hs : s⁻¹.Nonempty) (f : αβ) :
Finset.inf' s⁻¹ hs f = Finset.inf' s fun (x : α) => f x⁻¹
theorem Finset.image_op_neg {α : Type u_2} [] [Neg α] (s : ) :
theorem Finset.image_op_inv {α : Type u_2} [] [Inv α] (s : ) :
Finset.image MulOpposite.op s⁻¹ = (Finset.image MulOpposite.op s)⁻¹
@[simp]
theorem Finset.mem_neg' {α : Type u_2} [] [] {s : } {a : α} :
a -s -a s
@[simp]
theorem Finset.mem_inv' {α : Type u_2} [] [] {s : } {a : α} :
@[simp]
theorem Finset.coe_neg {α : Type u_2} [] [] (s : ) :
(-s) = -s
@[simp]
theorem Finset.coe_inv {α : Type u_2} [] [] (s : ) :
s⁻¹ = (s)⁻¹
@[simp]
theorem Finset.card_neg {α : Type u_2} [] [] (s : ) :
(-s).card = s.card
@[simp]
theorem Finset.card_inv {α : Type u_2} [] [] (s : ) :
s⁻¹.card = s.card
@[simp]
theorem Finset.preimage_neg {α : Type u_2} [] [] (s : ) :
Finset.preimage s (fun (x : α) => -x) = -s
@[simp]
theorem Finset.preimage_inv {α : Type u_2} [] [] (s : ) :
Finset.preimage s (fun (x : α) => x⁻¹) = s⁻¹
@[simp]
theorem Finset.neg_univ {α : Type u_2} [] [] [] :
-Finset.univ = Finset.univ
@[simp]
theorem Finset.inv_univ {α : Type u_2} [] [] [] :
Finset.univ⁻¹ = Finset.univ

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} [] [Mul α] :
Mul ()

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} [] [Add α] {s : } {t : } :
s + t = Finset.image (fun (p : α × α) => p.1 + p.2) (s ×ˢ t)
theorem Finset.mul_def {α : Type u_2} [] [Mul α] {s : } {t : } :
s * t = Finset.image (fun (p : α × α) => p.1 * p.2) (s ×ˢ t)
theorem Finset.image_add_product {α : Type u_2} [] [Add α] {s : } {t : } :
Finset.image (fun (x : α × α) => x.1 + x.2) (s ×ˢ t) = s + t
theorem Finset.image_mul_product {α : Type u_2} [] [Mul α] {s : } {t : } :
Finset.image (fun (x : α × α) => x.1 * x.2) (s ×ˢ t) = s * t
theorem Finset.mem_add {α : Type u_2} [] [Add α] {s : } {t : } {x : α} :
x s + t ∃ y ∈ s, ∃ z ∈ t, y + z = x
theorem Finset.mem_mul {α : Type u_2} [] [Mul α] {s : } {t : } {x : α} :
x s * t ∃ y ∈ s, ∃ z ∈ t, y * z = x
@[simp]
theorem Finset.coe_add {α : Type u_2} [] [Add α] (s : ) (t : ) :
(s + t) = s + t
@[simp]
theorem Finset.coe_mul {α : Type u_2} [] [Mul α] (s : ) (t : ) :
(s * t) = s * t
theorem Finset.add_mem_add {α : Type u_2} [] [Add α] {s : } {t : } {a : α} {b : α} :
a sb ta + b s + t
theorem Finset.mul_mem_mul {α : Type u_2} [] [Mul α] {s : } {t : } {a : α} {b : α} :
a sb ta * b s * t
theorem Finset.card_add_le {α : Type u_2} [] [Add α] {s : } {t : } :
(s + t).card s.card * t.card
theorem Finset.card_mul_le {α : Type u_2} [] [Mul α] {s : } {t : } :
(s * t).card s.card * t.card
theorem Finset.card_add_iff {α : Type u_2} [] [Add α] {s : } {t : } :
(s + t).card = s.card * t.card Set.InjOn (fun (p : α × α) => p.1 + p.2) (s ×ˢ t)
theorem Finset.card_mul_iff {α : Type u_2} [] [Mul α] {s : } {t : } :
(s * t).card = s.card * t.card Set.InjOn (fun (p : α × α) => p.1 * p.2) (s ×ˢ t)
@[simp]
theorem Finset.empty_add {α : Type u_2} [] [Add α] (s : ) :
@[simp]
theorem Finset.empty_mul {α : Type u_2} [] [Mul α] (s : ) :
@[simp]
theorem Finset.add_empty {α : Type u_2} [] [Add α] (s : ) :
@[simp]
theorem Finset.mul_empty {α : Type u_2} [] [Mul α] (s : ) :
@[simp]
theorem Finset.add_eq_empty {α : Type u_2} [] [Add α] {s : } {t : } :
s + t = s = t =
@[simp]
theorem Finset.mul_eq_empty {α : Type u_2} [] [Mul α] {s : } {t : } :
s * t = s = t =
@[simp]
theorem Finset.add_nonempty {α : Type u_2} [] [Add α] {s : } {t : } :
(s + t).Nonempty s.Nonempty t.Nonempty
@[simp]
theorem Finset.mul_nonempty {α : Type u_2} [] [Mul α] {s : } {t : } :
(s * t).Nonempty s.Nonempty t.Nonempty
theorem Finset.Nonempty.add {α : Type u_2} [] [Add α] {s : } {t : } :
s.Nonemptyt.Nonempty(s + t).Nonempty
theorem Finset.Nonempty.mul {α : Type u_2} [] [Mul α] {s : } {t : } :
s.Nonemptyt.Nonempty(s * t).Nonempty
theorem Finset.Nonempty.of_add_left {α : Type u_2} [] [Add α] {s : } {t : } :
(s + t).Nonemptys.Nonempty
theorem Finset.Nonempty.of_mul_left {α : Type u_2} [] [Mul α] {s : } {t : } :
(s * t).Nonemptys.Nonempty
theorem Finset.Nonempty.of_add_right {α : Type u_2} [] [Add α] {s : } {t : } :
(s + t).Nonemptyt.Nonempty
theorem Finset.Nonempty.of_mul_right {α : Type u_2} [] [Mul α] {s : } {t : } :
(s * t).Nonemptyt.Nonempty
theorem Finset.add_singleton {α : Type u_2} [] [Add α] {s : } (a : α) :
s + {a} = Finset.image (fun (x : α) => x + a) s
theorem Finset.mul_singleton {α : Type u_2} [] [Mul α] {s : } (a : α) :
s * {a} = Finset.image (fun (x : α) => x * a) s
theorem Finset.singleton_add {α : Type u_2} [] [Add α] {s : } (a : α) :
{a} + s = Finset.image (fun (x : α) => a + x) s
theorem Finset.singleton_mul {α : Type u_2} [] [Mul α] {s : } (a : α) :
{a} * s = Finset.image (fun (x : α) => a * x) s
@[simp]
theorem Finset.singleton_add_singleton {α : Type u_2} [] [Add α] (a : α) (b : α) :
{a} + {b} = {a + b}
@[simp]
theorem Finset.singleton_mul_singleton {α : Type u_2} [] [Mul α] (a : α) (b : α) :
{a} * {b} = {a * b}
theorem Finset.add_subset_add {α : Type u_2} [] [Add α] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
s₁ s₂t₁ t₂s₁ + t₁ s₂ + t₂
theorem Finset.mul_subset_mul {α : Type u_2} [] [Mul α] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
s₁ s₂t₁ t₂s₁ * t₁ s₂ * t₂
theorem Finset.add_subset_add_left {α : Type u_2} [] [Add α] {s : } {t₁ : } {t₂ : } :
t₁ t₂s + t₁ s + t₂
theorem Finset.mul_subset_mul_left {α : Type u_2} [] [Mul α] {s : } {t₁ : } {t₂ : } :
t₁ t₂s * t₁ s * t₂
theorem Finset.add_subset_add_right {α : Type u_2} [] [Add α] {s₁ : } {s₂ : } {t : } :
s₁ s₂s₁ + t s₂ + t
theorem Finset.mul_subset_mul_right {α : Type u_2} [] [Mul α] {s₁ : } {s₂ : } {t : } :
s₁ s₂s₁ * t s₂ * t
theorem Finset.add_subset_iff {α : Type u_2} [] [Add α] {s : } {t : } {u : } :
s + t u xs, yt, x + y u
theorem Finset.mul_subset_iff {α : Type u_2} [] [Mul α] {s : } {t : } {u : } :
s * t u xs, yt, x * y u
theorem Finset.union_add {α : Type u_2} [] [Add α] {s₁ : } {s₂ : } {t : } :
s₁ s₂ + t = s₁ + t (s₂ + t)
theorem Finset.union_mul {α : Type u_2} [] [Mul α] {s₁ : } {s₂ : } {t : } :
(s₁ s₂) * t = s₁ * t s₂ * t
theorem Finset.add_union {α : Type u_2} [] [Add α] {s : } {t₁ : } {t₂ : } :
s + (t₁ t₂) = s + t₁ (s + t₂)
theorem Finset.mul_union {α : Type u_2} [] [Mul α] {s : } {t₁ : } {t₂ : } :
s * (t₁ t₂) = s * t₁ s * t₂
theorem Finset.inter_add_subset {α : Type u_2} [] [Add α] {s₁ : } {s₂ : } {t : } :
s₁ s₂ + t (s₁ + t) (s₂ + t)
theorem Finset.inter_mul_subset {α : Type u_2} [] [Mul α] {s₁ : } {s₂ : } {t : } :
s₁ s₂ * t s₁ * t (s₂ * t)
theorem Finset.add_inter_subset {α : Type u_2} [] [Add α] {s : } {t₁ : } {t₂ : } :
s + t₁ t₂ (s + t₁) (s + t₂)
theorem Finset.mul_inter_subset {α : Type u_2} [] [Mul α] {s : } {t₁ : } {t₂ : } :
s * (t₁ t₂) s * t₁ (s * t₂)
theorem Finset.inter_add_union_subset_union {α : Type u_2} [] [Add α] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
s₁ s₂ + (t₁ t₂) s₁ + t₁ (s₂ + t₂)
theorem Finset.inter_mul_union_subset_union {α : Type u_2} [] [Mul α] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
s₁ s₂ * (t₁ t₂) s₁ * t₁ s₂ * t₂
theorem Finset.union_add_inter_subset_union {α : Type u_2} [] [Add α] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
s₁ s₂ + t₁ t₂ s₁ + t₁ (s₂ + t₂)
theorem Finset.union_mul_inter_subset_union {α : Type u_2} [] [Mul α] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
(s₁ s₂) * (t₁ t₂) s₁ * t₁ s₂ * t₂
theorem Finset.subset_add {α : Type u_2} [] [Add α] {u : } {s : Set α} {t : Set α} :
u s + t∃ (s' : ) (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} [] [Mul α] {u : } {s : Set α} {t : Set α} :
u s * t∃ (s' : ) (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} [] [] [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) {s : } {t : } :
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} [] [] [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (f : F) {s : } {t : } :
Finset.image (f) (s * t) = Finset.image (f) s * Finset.image (f) t

The singleton operation as an AddHom.

Equations
Instances For
∀ (x x_1 : α), {x + x_1} = {x} + {x_1}
def Finset.singletonMulHom {α : Type u_2} [] [Mul α] :

The singleton operation as a MulHom.

Equations
• Finset.singletonMulHom = { toFun := singleton, map_mul' := }
Instances For
@[simp]
@[simp]
theorem Finset.coe_singletonMulHom {α : Type u_2} [] [Mul α] :
Finset.singletonMulHom = singleton
@[simp]
theorem Finset.singletonAddHom_apply {α : Type u_2} [] [Add α] (a : α) :
@[simp]
theorem Finset.singletonMulHom_apply {α : Type u_2} [] [Mul α] (a : α) :
Finset.singletonMulHom a = {a}
def Finset.imageAddHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) :

Lift an AddHom to Finset via image

Equations
• = { toFun := , map_add' := }
Instances For
theorem Finset.imageAddHom.proof_1 {F : Type u_3} {α : Type u_1} {β : Type u_2} [] [] [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) :
∀ (x x_1 : ), Finset.image (f) (x + x_1) = Finset.image (f) x + Finset.image (f) x_1
@[simp]
theorem Finset.imageAddHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) (s : ) :
s = Finset.image (f) s
@[simp]
theorem Finset.imageMulHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (f : F) (s : ) :
s = Finset.image (f) s
def Finset.imageMulHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (f : F) :

Lift a MulHom to Finset via image.

Equations
• = { toFun := , map_mul' := }
Instances For
@[simp]
theorem Finset.sup_add_le {α : Type u_2} {β : Type u_3} [] [Add α] [] [] {s : } {t : } {f : αβ} {a : β} :
Finset.sup (s + t) f a xs, yt, f (x + y) a
@[simp]
theorem Finset.sup_mul_le {α : Type u_2} {β : Type u_3} [] [Mul α] [] [] {s : } {t : } {f : αβ} {a : β} :
Finset.sup (s * t) f a xs, yt, f (x * y) a
theorem Finset.sup_add_left {α : Type u_2} {β : Type u_3} [] [Add α] [] [] (s : ) (t : ) (f : αβ) :
Finset.sup (s + t) f = Finset.sup s fun (x : α) => Finset.sup t fun (x_1 : α) => f (x + x_1)
theorem Finset.sup_mul_left {α : Type u_2} {β : Type u_3} [] [Mul α] [] [] (s : ) (t : ) (f : αβ) :
Finset.sup (s * t) f = Finset.sup s fun (x : α) => Finset.sup t fun (x_1 : α) => f (x * x_1)
theorem Finset.sup_add_right {α : Type u_2} {β : Type u_3} [] [Add α] [] [] (s : ) (t : ) (f : αβ) :
Finset.sup (s + t) f = Finset.sup t fun (y : α) => Finset.sup s fun (x : α) => f (x + y)
theorem Finset.sup_mul_right {α : Type u_2} {β : Type u_3} [] [Mul α] [] [] (s : ) (t : ) (f : αβ) :
Finset.sup (s * t) f = Finset.sup t fun (y : α) => Finset.sup s fun (x : α) => f (x * y)
@[simp]
theorem Finset.le_inf_add {α : Type u_2} {β : Type u_3} [] [Add α] [] [] {s : } {t : } {f : αβ} {a : β} :
a Finset.inf (s + t) f xs, yt, a f (x + y)
@[simp]
theorem Finset.le_inf_mul {α : Type u_2} {β : Type u_3} [] [Mul α] [] [] {s : } {t : } {f : αβ} {a : β} :
a Finset.inf (s * t) f xs, yt, a f (x * y)
theorem Finset.inf_add_left {α : Type u_2} {β : Type u_3} [] [Add α] [] [] (s : ) (t : ) (f : αβ) :
Finset.inf (s + t) f = Finset.inf s fun (x : α) => Finset.inf t fun (x_1 : α) => f (x + x_1)
theorem Finset.inf_mul_left {α : Type u_2} {β : Type u_3} [] [Mul α] [] [] (s : ) (t : ) (f : αβ) :
Finset.inf (s * t) f = Finset.inf s fun (x : α) => Finset.inf t fun (x_1 : α) => f (x * x_1)
theorem Finset.inf_add_right {α : Type u_2} {β : Type u_3} [] [Add α] [] [] (s : ) (t : ) (f : αβ) :
Finset.inf (s + t) f = Finset.inf t fun (y : α) => Finset.inf s fun (x : α) => f (x + y)
theorem Finset.inf_mul_right {α : Type u_2} {β : Type u_3} [] [Mul α] [] [] (s : ) (t : ) (f : αβ) :
Finset.inf (s * t) f = Finset.inf t fun (y : α) => Finset.inf s fun (x : α) => f (x * y)

### Finset subtraction/division #

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

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} [] [Div α] :
Div ()

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} [] [Sub α] {s : } {t : } :
s - t = Finset.image (fun (p : α × α) => p.1 - p.2) (s ×ˢ t)
theorem Finset.div_def {α : Type u_2} [] [Div α] {s : } {t : } :
s / t = Finset.image (fun (p : α × α) => p.1 / p.2) (s ×ˢ t)
theorem Finset.image_sub_product {α : Type u_2} [] [Sub α] {s : } {t : } :
Finset.image (fun (x : α × α) => x.1 - x.2) (s ×ˢ t) = s - t
theorem Finset.image_div_product {α : Type u_2} [] [Div α] {s : } {t : } :
Finset.image (fun (x : α × α) => x.1 / x.2) (s ×ˢ t) = s / t
theorem Finset.mem_sub {α : Type u_2} [] [Sub α] {s : } {t : } {a : α} :
a s - t ∃ b ∈ s, ∃ c ∈ t, b - c = a
theorem Finset.mem_div {α : Type u_2} [] [Div α] {s : } {t : } {a : α} :
a s / t ∃ b ∈ s, ∃ c ∈ t, b / c = a
@[simp]
theorem Finset.coe_sub {α : Type u_2} [] [Sub α] (s : ) (t : ) :
(s - t) = s - t
@[simp]
theorem Finset.coe_div {α : Type u_2} [] [Div α] (s : ) (t : ) :
(s / t) = s / t
theorem Finset.sub_mem_sub {α : Type u_2} [] [Sub α] {s : } {t : } {a : α} {b : α} :
a sb ta - b s - t
theorem Finset.div_mem_div {α : Type u_2} [] [Div α] {s : } {t : } {a : α} {b : α} :
a sb ta / b s / t
theorem Finset.sub_card_le {α : Type u_2} [] [Sub α] {s : } {t : } :
(s - t).card s.card * t.card
theorem Finset.div_card_le {α : Type u_2} [] [Div α] {s : } {t : } :
(s / t).card s.card * t.card
@[simp]
theorem Finset.empty_sub {α : Type u_2} [] [Sub α] (s : ) :
@[simp]
theorem Finset.empty_div {α : Type u_2} [] [Div α] (s : ) :
@[simp]
theorem Finset.sub_empty {α : Type u_2} [] [Sub α] (s : ) :
@[simp]
theorem Finset.div_empty {α : Type u_2} [] [Div α] (s : ) :
@[simp]
theorem Finset.sub_eq_empty {α : Type u_2} [] [Sub α] {s : } {t : } :
s - t = s = t =
@[simp]
theorem Finset.div_eq_empty {α : Type u_2} [] [Div α] {s : } {t : } :
s / t = s = t =
@[simp]
theorem Finset.sub_nonempty {α : Type u_2} [] [Sub α] {s : } {t : } :
(s - t).Nonempty s.Nonempty t.Nonempty
@[simp]
theorem Finset.div_nonempty {α : Type u_2} [] [Div α] {s : } {t : } :
(s / t).Nonempty s.Nonempty t.Nonempty
theorem Finset.Nonempty.sub {α : Type u_2} [] [Sub α] {s : } {t : } :
s.Nonemptyt.Nonempty(s - t).Nonempty
theorem Finset.Nonempty.div {α : Type u_2} [] [Div α] {s : } {t : } :
s.Nonemptyt.Nonempty(s / t).Nonempty
theorem Finset.Nonempty.of_sub_left {α : Type u_2} [] [Sub α] {s : } {t : } :
(s - t).Nonemptys.Nonempty
theorem Finset.Nonempty.of_div_left {α : Type u_2} [] [Div α] {s : } {t : } :
(s / t).Nonemptys.Nonempty
theorem Finset.Nonempty.of_sub_right {α : Type u_2} [] [Sub α] {s : } {t : } :
(s - t).Nonemptyt.Nonempty
theorem Finset.Nonempty.of_div_right {α : Type u_2} [] [Div α] {s : } {t : } :
(s / t).Nonemptyt.Nonempty
@[simp]
theorem Finset.sub_singleton {α : Type u_2} [] [Sub α] {s : } (a : α) :
s - {a} = Finset.image (fun (x : α) => x - a) s
@[simp]
theorem Finset.div_singleton {α : Type u_2} [] [Div α] {s : } (a : α) :
s / {a} = Finset.image (fun (x : α) => x / a) s
@[simp]
theorem Finset.singleton_sub {α : Type u_2} [] [Sub α] {s : } (a : α) :
{a} - s = Finset.image (fun (x : α) => a - x) s
@[simp]
theorem Finset.singleton_div {α : Type u_2} [] [Div α] {s : } (a : α) :
{a} / s = Finset.image (fun (x : α) => a / x) s
theorem Finset.singleton_sub_singleton {α : Type u_2} [] [Sub α] (a : α) (b : α) :
{a} - {b} = {a - b}
theorem Finset.singleton_div_singleton {α : Type u_2} [] [Div α] (a : α) (b : α) :
{a} / {b} = {a / b}
theorem Finset.sub_subset_sub {α : Type u_2} [] [Sub α] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
s₁ s₂t₁ t₂s₁ - t₁ s₂ - t₂
theorem Finset.div_subset_div {α : Type u_2} [] [Div α] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
s₁ s₂t₁ t₂s₁ / t₁ s₂ / t₂
theorem Finset.sub_subset_sub_left {α : Type u_2} [] [Sub α] {s : } {t₁ : } {t₂ : } :
t₁ t₂s - t₁ s - t₂
theorem Finset.div_subset_div_left {α : Type u_2} [] [Div α] {s : } {t₁ : } {t₂ : } :
t₁ t₂s / t₁ s / t₂
theorem Finset.sub_subset_sub_right {α : Type u_2} [] [Sub α] {s₁ : } {s₂ : } {t : } :
s₁ s₂s₁ - t s₂ - t
theorem Finset.div_subset_div_right {α : Type u_2} [] [Div α] {s₁ : } {s₂ : } {t : } :
s₁ s₂s₁ / t s₂ / t
theorem Finset.sub_subset_iff {α : Type u_2} [] [Sub α] {s : } {t : } {u : } :
s - t u xs, yt, x - y u
theorem Finset.div_subset_iff {α : Type u_2} [] [Div α] {s : } {t : } {u : } :
s / t u xs, yt, x / y u
theorem Finset.union_sub {α : Type u_2} [] [Sub α] {s₁ : } {s₂ : } {t : } :
s₁ s₂ - t = s₁ - t (s₂ - t)
theorem Finset.union_div {α : Type u_2} [] [Div α] {s₁ : } {s₂ : } {t : } :
(s₁ s₂) / t = s₁ / t s₂ / t
theorem Finset.sub_union {α : Type u_2} [] [Sub α] {s : } {t₁ : } {t₂ : } :
s - (t₁ t₂) = s - t₁ (s - t₂)
theorem Finset.div_union {α : Type u_2} [] [Div α] {s : } {t₁ : } {t₂ : } :
s / (t₁ t₂) = s / t₁ s / t₂
theorem Finset.inter_sub_subset {α : Type u_2} [] [Sub α] {s₁ : } {s₂ : } {t : } :
s₁ s₂ - t (s₁ - t) (s₂ - t)
theorem Finset.inter_div_subset {α : Type u_2} [] [Div α] {s₁ : } {s₂ : } {t : } :
s₁ s₂ / t s₁ / t (s₂ / t)
theorem Finset.sub_inter_subset {α : Type u_2} [] [Sub α] {s : } {t₁ : } {t₂ : } :
s - t₁ t₂ (s - t₁) (s - t₂)
theorem Finset.div_inter_subset {α : Type u_2} [] [Div α] {s : } {t₁ : } {t₂ : } :
s / (t₁ t₂) s / t₁ (s / t₂)
theorem Finset.inter_sub_union_subset_union {α : Type u_2} [] [Sub α] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
s₁ s₂ - (t₁ t₂) s₁ - t₁ (s₂ - t₂)
theorem Finset.inter_div_union_subset_union {α : Type u_2} [] [Div α] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
s₁ s₂ / (t₁ t₂) s₁ / t₁ s₂ / t₂
theorem Finset.union_sub_inter_subset_union {α : Type u_2} [] [Sub α] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
s₁ s₂ - t₁ t₂ s₁ - t₁ (s₂ - t₂)
theorem Finset.union_div_inter_subset_union {α : Type u_2} [] [Div α] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
(s₁ s₂) / (t₁ t₂) s₁ / t₁ s₂ / t₂
theorem Finset.subset_sub {α : Type u_2} [] [Sub α] {u : } {s : Set α} {t : Set α} :
u s - t∃ (s' : ) (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} [] [Div α] {u : } {s : Set α} {t : Set α} :
u s / t∃ (s' : ) (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'.

@[simp]
theorem Finset.sup_sub_le {α : Type u_2} {β : Type u_3} [] [Sub α] [] [] {s : } {t : } {f : αβ} {a : β} :
Finset.sup (s - t) f a xs, yt, f (x - y) a
@[simp]
theorem Finset.sup_div_le {α : Type u_2} {β : Type u_3} [] [Div α] [] [] {s : } {t : } {f : αβ} {a : β} :
Finset.sup (s / t) f a xs, yt, f (x / y) a
theorem Finset.sup_sub_left {α : Type u_2} {β : Type u_3} [] [Sub α] [] [] (s : ) (t : ) (f : αβ) :
Finset.sup (s - t) f = Finset.sup s fun (x : α) => Finset.sup t fun (x_1 : α) => f (x - x_1)
theorem Finset.sup_div_left {α : Type u_2} {β : Type u_3} [] [Div α] [] [] (s : ) (t : ) (f : αβ) :
Finset.sup (s / t) f = Finset.sup s fun (x : α) => Finset.sup t fun (x_1 : α) => f (x / x_1)
theorem Finset.sup_sub_right {α : Type u_2} {β : Type u_3} [] [Sub α] [] [] (s : ) (t : ) (f : αβ) :
Finset.sup (s - t) f = Finset.sup t fun (y : α) => Finset.sup s fun (x : α) => f (x - y)
theorem Finset.sup_div_right {α : Type u_2} {β : Type u_3} [] [Div α] [] [] (s : ) (t : ) (f : αβ) :
Finset.sup (s / t) f = Finset.sup t fun (y : α) => Finset.sup s fun (x : α) => f (x / y)
@[simp]
theorem Finset.le_inf_sub {α : Type u_2} {β : Type u_3} [] [Sub α] [] [] {s : } {t : } {f : αβ} {a : β} :
a Finset.inf (s - t) f xs, yt, a f (x - y)
@[simp]
theorem Finset.le_inf_div {α : Type u_2} {β : Type u_3} [] [Div α] [] [] {s : } {t : } {f : αβ} {a : β} :
a Finset.inf (s / t) f xs, yt, a f (x / y)
theorem Finset.inf_sub_left {α : Type u_2} {β : Type u_3} [] [Sub α] [] [] (s : ) (t : ) (f : αβ) :
Finset.inf (s - t) f = Finset.inf s fun (x : α) => Finset.inf t fun (x_1 : α) => f (x - x_1)
theorem Finset.inf_div_left {α : Type u_2} {β : Type u_3} [] [Div α] [] [] (s : ) (t : ) (f : αβ) :
Finset.inf (s / t) f = Finset.inf s fun (x : α) => Finset.inf t fun (x_1 : α) => f (x / x_1)
theorem Finset.inf_sub_right {α : Type u_2} {β : Type u_3} [] [Sub α] [] [] (s : ) (t : ) (f : αβ) :
Finset.inf (s - t) f = Finset.inf t fun (y : α) => Finset.inf s fun (x : α) => f (x - y)
theorem Finset.inf_div_right {α : Type u_2} {β : Type u_3} [] [Div α] [] [] (s : ) (t : ) (f : αβ) :
Finset.inf (s / t) f = Finset.inf t fun (y : α) => Finset.inf s fun (x : α) => f (x / y)

### Instances #

def Finset.nsmul {α : Type u_2} [] [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} [] [One α] [Mul α] :
Pow ()

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} [] [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} [] [One α] [Mul α] [Inv α] :
Pow ()

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 npowRec n s }
Instances For
def Finset.addSemigroup {α : Type u_2} [] [] :

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

Equations
Instances For
theorem Finset.addSemigroup.proof_1 {α : Type u_1} [] [] (s : ) (t : ) :
(s + t) = s + t
def Finset.semigroup {α : Type u_2} [] [] :

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

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

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

Equations
Instances For
def Finset.commSemigroup {α : Type u_2} [] [] :

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

Equations
Instances For
theorem Finset.inter_add_union_subset {α : Type u_2} [] [] {s : } {t : } :
s t + (s t) s + t
theorem Finset.inter_mul_union_subset {α : Type u_2} [] [] {s : } {t : } :
s t * (s t) s * t
theorem Finset.union_add_inter_subset {α : Type u_2} [] [] {s : } {t : } :
s t + s t s + t
theorem Finset.union_mul_inter_subset {α : Type u_2} [] [] {s : } {t : } :
(s t) * (s t) s * t
def Finset.addZeroClass {α : Type u_2} [] [] :

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

Equations
Instances For
theorem Finset.addZeroClass.proof_2 {α : Type u_1} [] [] (s : ) (t : ) :
(s + t) = s + t
theorem Finset.addZeroClass.proof_1 {α : Type u_1} [] :
{0} = {0}
def Finset.mulOneClass {α : Type u_2} [] [] :

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

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

The singleton operation as an AddMonoidHom.

Equations
• Finset.singletonAddMonoidHom = let __src := Finset.singletonAddHom; let __src_1 := Finset.singletonZeroHom; { toZeroHom := { toFun := __src.toFun, map_zero' := }, map_add' := }
Instances For
def Finset.singletonMonoidHom {α : Type u_2} [] [] :
α →*

The singleton operation as a MonoidHom.

Equations
• Finset.singletonMonoidHom = let __src := Finset.singletonMulHom; let __src_1 := Finset.singletonOneHom; { toOneHom := { toFun := __src.toFun, map_one' := }, map_mul' := }
Instances For
@[simp]
theorem Finset.coe_singletonAddMonoidHom {α : Type u_2} [] [] :
@[simp]
theorem Finset.coe_singletonMonoidHom {α : Type u_2} [] [] :
Finset.singletonMonoidHom = singleton
@[simp]
theorem Finset.singletonAddMonoidHom_apply {α : Type u_2} [] [] (a : α) :
@[simp]
theorem Finset.singletonMonoidHom_apply {α : Type u_2} [] [] (a : α) :
Finset.singletonMonoidHom a = {a}
noncomputable def Finset.coeAddMonoidHom {α : Type u_2} [] [] :
→+ Set α

The coercion from Finset to set as an AddMonoidHom.

Equations
• Finset.coeAddMonoidHom = { toZeroHom := { toFun := CoeTC.coe, map_zero' := }, map_add' := }
Instances For
theorem Finset.coeAddMonoidHom.proof_1 {α : Type u_1} [] :
0 = 0
theorem Finset.coeAddMonoidHom.proof_2 {α : Type u_1} [] [] (s : ) (t : ) :
(s + t) = s + t
noncomputable def Finset.coeMonoidHom {α : Type u_2} [] [] :
→* Set α

The coercion from Finset to Set as a MonoidHom.

Equations
• Finset.coeMonoidHom = { toOneHom := { toFun := CoeTC.coe, map_one' := }, map_mul' := }
Instances For
@[simp]
theorem Finset.coe_coeAddMonoidHom {α : Type u_2} [] [] :
@[simp]
theorem Finset.coe_coeMonoidHom {α : Type u_2} [] [] :
Finset.coeMonoidHom = CoeTC.coe
@[simp]
theorem Finset.coeAddMonoidHom_apply {α : Type u_2} [] [] (s : ) :
@[simp]
theorem Finset.coeMonoidHom_apply {α : Type u_2} [] [] (s : ) :
Finset.coeMonoidHom s = s
theorem Finset.imageAddMonoidHom.proof_2 {F : Type u_3} {α : Type u_1} {β : Type u_2} [] [] [] [] [FunLike F α β] [] (f : F) (x : ) (y : ) :
.toFun (x + y) = .toFun x + .toFun y
theorem Finset.imageAddMonoidHom.proof_1 {F : Type u_3} {α : Type u_2} {β : Type u_1} [] [] [] [FunLike F α β] [] (f : F) :
.toFun 0 = 0
def Finset.imageAddMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] [] [FunLike F α β] [] (f : F) :

Lift an add_monoid_hom to Finset via image

Equations
• = let __src := ; let __src_1 := ; { toZeroHom := { toFun := __src.toFun, map_zero' := }, map_add' := }
Instances For
@[simp]
theorem Finset.imageMonoidHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] [] [FunLike F α β] [] (f : F) :
∀ (a : ), = .toFun a
@[simp]
theorem Finset.imageAddMonoidHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] [] [FunLike F α β] [] (f : F) :
∀ (a : ), = .toFun a
def Finset.imageMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] [] [FunLike F α β] [] (f : F) :

Lift a MonoidHom to Finset via image.

Equations
• = let __src := ; let __src_1 := ; { toOneHom := { toFun := __src.toFun, map_one' := }, map_mul' := }
Instances For
@[simp]
theorem Finset.coe_nsmul {α : Type u_2} [] [] (s : ) (n : ) :
(n s) = n s
@[simp]
theorem Finset.coe_pow {α : Type u_2} [] [] (s : ) (n : ) :
(s ^ n) = s ^ n
theorem Finset.addMonoid.proof_3 {α : Type u_1} [] [] (s : ) (n : ) :
(n s) = n s
def Finset.addMonoid {α : Type u_2} [] [] :

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

Equations
Instances For
theorem Finset.addMonoid.proof_2 {α : Type u_1} [] [] (s : ) (t : ) :
(s + t) = s + t
theorem Finset.addMonoid.proof_1 {α : Type u_1} [] :
0 = 0
def Finset.monoid {α : Type u_2} [] [] :

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

Equations
Instances For
abbrev Finset.nsmul_mem_nsmul.match_1 (motive : ) :
∀ (x : ), (Unitmotive 0)(∀ (n : ), motive ())motive x
Equations
• =
Instances For
theorem Finset.nsmul_mem_nsmul {α : Type u_2} [] [] {s : } {a : α} (ha : a s) (n : ) :
n a n s
theorem Finset.pow_mem_pow {α : Type u_2} [] [] {s : } {a : α} (ha : a s) (n : ) :
a ^ n s ^ n
theorem Finset.nsmul_subset_nsmul {α : Type u_2} [] [] {s : } {t : } (hst : s t) (n : ) :
n s n t
theorem Finset.pow_subset_pow {α : Type u_2} [] [] {s : } {t : } (hst : s t) (n : ) :
s ^ n t ^ n
theorem Finset.nsmul_subset_nsmul_of_zero_mem {α : Type u_2} [] [] {s : } {m : } {n : } (hs : 0 s) :
m nm s n s
theorem Finset.pow_subset_pow_of_one_mem {α : Type u_2} [] [] {s : } {m : } {n : } (hs : 1 s) :
m ns ^ m s ^ n
@[simp]
theorem Finset.coe_list_sum {α : Type u_2} [] [] (s : List ()) :
() = List.sum (List.map Finset.toSet s)
@[simp]
theorem Finset.coe_list_prod {α : Type u_2} [] [] (s : List ()) :
() = List.prod (List.map Finset.toSet s)
theorem Finset.mem_sum_list_ofFn {α : Type u_2} [] [] {n : } {a : α} {s : Fin n} :
a ∃ (f : (i : Fin n) → { x : α // x s i }), List.sum (List.ofFn fun (i : Fin n) => (f i)) = a
theorem Finset.mem_prod_list_ofFn {α : Type u_2} [] [] {n : } {a : α} {s : Fin n} :
a ∃ (f : (i : Fin n) → { x : α // x s i }), List.prod (List.ofFn fun (i : Fin n) => (f i)) = a
theorem Finset.mem_nsmul {α : Type u_2} [] [] {s : } {a : α} {n : } :
a n s ∃ (f : Fin n{ x : α // x s }), List.sum (List.ofFn fun (i : Fin n) => (f i)) = a
theorem Finset.mem_pow {α : Type u_2} [] [] {s : } {a : α} {n : } :
a s ^ n ∃ (f : Fin n{ x : α // x s }), List.prod (List.ofFn fun (i : Fin n) => (f i)) = a
@[simp]
theorem Finset.empty_nsmul {α : Type u_2} [] [] {n : } (hn : n 0) :
@[simp]
theorem Finset.empty_pow {α : Type u_2} [] [] {n : } (hn : n 0) :
theorem Finset.add_univ_of_zero_mem {α : Type u_2} [] [] {s : } [] (hs : 0 s) :
s + Finset.univ = Finset.univ
theorem Finset.mul_univ_of_one_mem {α : Type u_2} [] [] {s : } [] (hs : 1 s) :
s * Finset.univ = Finset.univ
theorem Finset.univ_add_of_zero_mem {α : Type u_2} [] [] {t : } [] (ht : 0 t) :
Finset.univ + t = Finset.univ
theorem Finset.univ_mul_of_one_mem {α : Type u_2} [] [] {t : } [] (ht : 1 t) :
Finset.univ * t = Finset.univ
@[simp]
theorem Finset.univ_add_univ {α : Type u_2} [] [] [] :
Finset.univ + Finset.univ = Finset.univ
@[simp]
theorem Finset.univ_mul_univ {α : Type u_2} [] [] [] :
Finset.univ * Finset.univ = Finset.univ
@[simp]
theorem Finset.nsmul_univ {α : Type u_2} [] [] {n : } [] (hn : n 0) :
n Finset.univ = Finset.univ
@[simp]
theorem Finset.univ_pow {α : Type u_2} [] [] {n : } [] (hn : n 0) :
Finset.univ ^ n = Finset.univ
theorem IsAddUnit.finset {α : Type u_2} [] [] {a : α} :
theorem IsUnit.finset {α : Type u_2} [] [] {a : α} :
IsUnit {a}
theorem Finset.addCommMonoid.proof_2 {α : Type u_1} [] [] (s : ) (t : ) :
(s + t) = s + t
theorem Finset.addCommMonoid.proof_3 {α : Type u_1} [] [] (s : ) (n : ) :
(n s) = n s
theorem Finset.addCommMonoid.proof_1 {α : Type u_1} [] :
0 = 0
def Finset.addCommMonoid {α : Type u_2} [] [] :

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

Equations
Instances For
def Finset.commMonoid {α : Type u_2} [] [] :

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

Equations
Instances For
@[simp]
theorem Finset.coe_sum {α : Type u_2} [] [] {ι : Type u_5} (s : ) (f : ι) :
(Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => (f i)
@[simp]
theorem Finset.coe_prod {α : Type u_2} [] [] {ι : Type u_5} (s : ) (f : ι) :
(Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => (f i)
abbrev Finset.coe_zsmul.match_1 (motive : ) :
∀ (x : ), (∀ (n : ), motive ())(∀ (n : ), motive ())motive x
Equations
• =
Instances For
@[simp]
theorem Finset.coe_zsmul {α : Type u_2} [] (s : ) (n : ) :
(n s) = n s
@[simp]
theorem Finset.coe_zpow {α : Type u_2} [] [] (s : ) (n : ) :
(s ^ n) = s ^ n
theorem Finset.add_eq_zero_iff {α : Type u_2} [] {s : } {t : } :
s + t = 0 ∃ (a : α) (b : α), s = {a} t = {b} a + b = 0
theorem Finset.mul_eq_one_iff {α : Type u_2} [] [] {s : } {t : } :
s * t = 1 ∃ (a : α) (b : α), s = {a} t = {b} a * b = 1
theorem Finset.subtractionMonoid.proof_3 {α : Type u_1} [] (s : ) :
(-s) = -s
def Finset.subtractionMonoid {α : Type u_2} [] :

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

Equations
Instances For
theorem Finset.subtractionMonoid.proof_1 {α : Type u_1} :
0 = 0
theorem Finset.subtractionMonoid.proof_6 {α : Type u_1} [] (s : ) (n : ) :
(n s) = n s
theorem Finset.subtractionMonoid.proof_2 {α : Type u_1} [] (s : ) (t : ) :
(s + t) = s + t
theorem Finset.subtractionMonoid.proof_4 {α : Type u_1} [] (s : ) (t : ) :
(s - t) = s - t
theorem Finset.subtractionMonoid.proof_5 {α : Type u_1} [] (s : ) (n : ) :
(n s) = n s
def Finset.divisionMonoid {α : Type u_2} [] [] :

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

Equations
Instances For
@[simp]
theorem Finset.isAddUnit_iff {α : Type u_2} [] {s : } :
∃ (a : α), s = {a}
@[simp]
theorem Finset.isUnit_iff {α : Type u_2} [] [] {s : } :
∃ (a : α), s = {a}
@[simp]
theorem Finset.isAddUnit_coe {α : Type u_2} [] {s : } :
@[simp]
theorem Finset.isUnit_coe {α : Type u_2} [] [] {s : } :
IsUnit s
@[simp]
theorem Finset.univ_sub_univ {α : Type u_2} [] [] :
Finset.univ - Finset.univ = Finset.univ
@[simp]
theorem Finset.univ_div_univ {α : Type u_2} [] [] [] :
Finset.univ / Finset.univ = Finset.univ
theorem Finset.subtractionCommMonoid.proof_6 {α : Type u_1} [] (s : ) (n : ) :
(n s) = n s
theorem Finset.subtractionCommMonoid.proof_3 {α : Type u_1} [] (s : ) :
(-s) = -s

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

Equations
Instances For
theorem Finset.subtractionCommMonoid.proof_4 {α : Type u_1} [] (s : ) (t : ) :
(s - t) = s - t
theorem Finset.subtractionCommMonoid.proof_5 {α : Type u_1} [] (s : ) (n : ) :
(n s) = n s
theorem Finset.subtractionCommMonoid.proof_2 {α : Type u_1} [] (s : ) (t : ) :
(s + t) = s + t
def Finset.divisionCommMonoid {α : Type u_2} [] :

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

Equations
Instances For
def Finset.distribNeg {α : Type u_2} [] [Mul α] [] :

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} [] [] (s : ) (t : ) (u : ) :
s * (t + u) s * t + s * u
theorem Finset.add_mul_subset {α : Type u_2} [] [] (s : ) (t : ) (u : ) :
(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} [] [] (s : ) :
s * 0 0
theorem Finset.zero_mul_subset {α : Type u_2} [] [] (s : ) :
0 * s 0
theorem Finset.Nonempty.mul_zero {α : Type u_2} [] [] {s : } (hs : s.Nonempty) :
s * 0 = 0
theorem Finset.Nonempty.zero_mul {α : Type u_2} [] [] {s : } (hs : s.Nonempty) :
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} [] [] {s : } {t : } :
0 s - t ¬Disjoint s t
@[simp]
theorem Finset.one_mem_div_iff {α : Type u_2} [] [] {s : } {t : } :
1 s / t ¬Disjoint s t
theorem Finset.not_zero_mem_sub_iff {α : Type u_2} [] [] {s : } {t : } :
0s - t Disjoint s t
theorem Finset.not_one_mem_div_iff {α : Type u_2} [] [] {s : } {t : } :
1s / t Disjoint s t
abbrev Finset.Nonempty.zero_mem_sub.match_1 {α : Type u_1} {s : } (motive : s.NonemptyProp) :
∀ (h : s.Nonempty), (∀ (a : α) (ha : a s), motive )motive h
Equations
• =
Instances For
theorem Finset.Nonempty.zero_mem_sub {α : Type u_2} [] [] {s : } (h : s.Nonempty) :
0 s - s
theorem Finset.Nonempty.one_mem_div {α : Type u_2} [] [] {s : } (h : s.Nonempty) :
1 s / s
theorem Finset.isAddUnit_singleton {α : Type u_2} [] [] (a : α) :
theorem Finset.isUnit_singleton {α : Type u_2} [] [] (a : α) :
IsUnit {a}
theorem Finset.isUnit_iff_singleton {α : Type u_2} [] [] {s : } :
∃ (a : α), s = {a}
@[simp]
theorem Finset.isUnit_iff_singleton_aux {α : Type u_2} [] {s : } :
(∃ (a : α), s = {a} ) ∃ (a : α), s = {a}
@[simp]
theorem Finset.image_add_left {α : Type u_2} [] [] {t : } {a : α} :
Finset.image (fun (b : α) => a + b) t = Finset.preimage t (fun (b : α) => -a + b)
@[simp]
theorem Finset.image_mul_left {α : Type u_2} [] [] {t : } {a : α} :
Finset.image (fun (b : α) => a * b) t = Finset.preimage t (fun (b : α) => a⁻¹ * b)
@[simp]
theorem Finset.image_add_right {α : Type u_2} [] [] {t : } {b : α} :
Finset.image (fun (x : α) => x + b) t = Finset.preimage t (fun (x : α) => x + -b)
@[simp]
theorem Finset.image_mul_right {α : Type u_2} [] [] {t : } {b : α} :
Finset.image (fun (x : α) => x * b) t = Finset.preimage t (fun (x : α) => x * b⁻¹)
theorem Finset.image_add_left' {α : Type u_2} [] [] {t : } {a : α} :
Finset.image (fun (b : α) => -a + b) t = Finset.preimage t (fun (b : α) => a + b)
theorem Finset.image_mul_left' {α : Type u_2} [] [] {t : } {a : α} :
Finset.image (fun (b : α) => a⁻¹ * b) t = Finset.preimage t (fun (b : α) => a * b)
theorem Finset.image_add_right' {α : Type u_2} [] [] {t : } {b : α} :
Finset.image (fun (x : α) => x + -b) t = Finset.preimage t (fun (x : α) => x + b)
theorem Finset.image_mul_right' {α : Type u_2} [] [] {t : } {b : α} :
Finset.image (fun (x : α) => x * b⁻¹) t = Finset.preimage t (fun (x : α) => x * b)
theorem Finset.image_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] [] [FunLike F α β] [] (f : F) {s : } {t : } :
Finset.image (f) (s / t) = Finset.image (f) s / Finset.image (f) t
theorem Finset.div_zero_subset {α : Type u_2} [] [] (s : ) :
s / 0 0
theorem Finset.zero_div_subset {α : Type u_2} [] [] (s : ) :
0 / s 0
theorem Finset.Nonempty.div_zero {α : Type u_2} [] [] {s : } (hs : s.Nonempty) :
s / 0 = 0
theorem Finset.Nonempty.zero_div {α : Type u_2} [] [] {s : } (hs : s.Nonempty) :
0 / s = 0
@[simp]
theorem Finset.preimage_add_left_singleton {α : Type u_2} [] {a : α} {b : α} :
Finset.preimage {b} (fun (x : α) => a + x) = {-a + b}
@[simp]
theorem Finset.preimage_mul_left_singleton {α : Type u_2} [] {a : α} {b : α} :
Finset.preimage {b} (fun (x : α) => a * x) = {a⁻¹ * b}
@[simp]
theorem Finset.preimage_add_right_singleton {α : Type u_2} [] {a : α} {b : α} :
Finset.preimage {b} (fun (x : α) => x + a) = {b + -a}
@[simp]
theorem Finset.preimage_mul_right_singleton {α : Type u_2} [] {a : α} {b : α} :
Finset.preimage {b} (fun (x : α) => x * a) = {b * a⁻¹}
@[simp]
theorem Finset.preimage_add_left_zero {α : Type u_2} [] {a : α} :
Finset.preimage 0 (fun (x : α) => a + x) = {-a}
@[simp]
theorem Finset.preimage_mul_left_one {α : Type u_2} [] {a : α} :
Finset.preimage 1 (fun (x : α) => a * x) = {a⁻¹}
@[simp]
theorem Finset.preimage_add_right_zero {α : Type u_2} [] {b : α} :
Finset.preimage 0 (fun (x : α) => x + b) = {-b}
@[simp]
theorem Finset.preimage_mul_right_one {α : Type u_2} [] {b : α} :
Finset.preimage 1 (fun (x : α) => x * b) = {b⁻¹}
theorem Finset.preimage_add_left_zero' {α : Type u_2} [] {a : α} :
Finset.preimage 0 (fun (x : α) => -a + x) = {a}
theorem Finset.preimage_mul_left_one' {α : Type u_2} [] {a : α} :
Finset.preimage 1 (fun (x : α) => a⁻¹ * x) = {a}
theorem Finset.preimage_add_right_zero' {α : Type u_2} [] {b : α} :
Finset.preimage 0 (fun (x : α) => x + -b) = {b}
theorem Finset.preimage_mul_right_one' {α : Type u_2} [] {b : α} :
Finset.preimage 1 (fun (x : α) => x * b⁻¹) = {b}

### Scalar addition/multiplication of finsets #

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

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} [] [SMul α β] :
SMul () ()

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} [] [VAdd α β] {s : } {t : } :
s +ᵥ t = Finset.image (fun (p : α × β) => p.1 +ᵥ p.2) (s ×ˢ t)
theorem Finset.smul_def {α : Type u_2} {β : Type u_3} [] [SMul α β] {s : } {t : } :
s t = Finset.image (fun (p : α × β) => p.1 p.2) (s ×ˢ t)
theorem Finset.image_vadd_product {α : Type u_2} {β : Type u_3} [] [VAdd α β] {s : } {t : } :
Finset.image (fun (x : α × β) => x.1 +ᵥ x.2) (s ×ˢ t) = s +ᵥ t
theorem Finset.image_smul_product {α : Type u_2} {β : Type u_3} [] [SMul α β] {s : } {t : } :
Finset.image (fun (x : α × β) => x.1 x.2) (s ×ˢ t) = s t
theorem Finset.mem_vadd {α : Type u_2} {β : Type u_3} [] [VAdd α β] {s : } {t : } {x : β} :
x s +ᵥ t ∃ y ∈ s, ∃ z ∈ t, y +ᵥ z = x
theorem Finset.mem_smul {α : Type u_2} {β : Type u_3} [] [SMul α β] {s : } {t : } {x : β} :
x s t ∃ y ∈ s, ∃ z ∈ t, y z = x
@[simp]
theorem Finset.coe_vadd {α : Type u_2} {β : Type u_3} [] [VAdd α β] (s : ) (t : ) :
(s +ᵥ t) = s +ᵥ t
@[simp]
theorem Finset.coe_smul {α : Type u_2} {β : Type u_3} [] [SMul α β] (s : ) (t : ) :
(s t) = s t
theorem Finset.vadd_mem_vadd {α : Type u_2} {β : Type u_3} [] [VAdd α β] {s : } {t : } {a : α} {b : β} :
a sb ta +ᵥ b s +ᵥ t
theorem Finset.smul_mem_smul {α : Type u_2} {β : Type u_3} [] [SMul α β] {s : } {t : } {a : α} {b : β} :
a sb ta b s t
theorem Finset.vadd_card_le {α : Type u_2} {β : Type u_3} [] [VAdd α β] {s : } {t : } :
(s +ᵥ t).card s.card t.card
theorem Finset.smul_card_le {α : Type u_2} {β : Type u_3} [] [SMul α β] {s : } {t : } :
(s t).card s.card t.card