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

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

0/1 as finsets

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

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

Equations

• Finset.zero = { zero := {0} }

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} }

@[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

theorem Finset.zero_nonempty {α : Type u_2} [Zero α] : Finset.Nonempty 0

theorem Finset.one_nonempty {α : Type u_2} [One α] : Finset.Nonempty 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 α] : Finset.card 0 = 1

@[simp]

theorem Finset.card_one {α : Type u_2} [One α] : Finset.card 1 = 1

def Finset.singletonZeroHom {α : Type u_2} [Zero α] : ZeroHom α (Finset α)

The singleton operation as a ZeroHom.

Equations

• Finset.singletonZeroHom = { toFun := singleton, map_zero' := (_ : {0} = 0) }

def Finset.singletonOneHom {α : Type u_2} [One α] : OneHom α (Finset α)

The singleton operation as a OneHom.

Equations

• Finset.singletonOneHom = { toFun := singleton, map_one' := (_ : {1} = 1) }

@[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) : ZeroHom (Finset α) (Finset β)

Lift a ZeroHom to Finset via image

Equations

• Finset.imageZeroHom f = { toFun := Finset.image ↑f, map_zero' := (_ : Finset.image (↑f) 0 = 0) }

@[simp]

theorem Finset.imageZeroHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [Zero α] [DecidableEq β] [Zero β] [ZeroHomClass F α β] (f : F) (s : Finset α) : ↑(Finset.imageZeroHom f) s = Finset.image (↑f) s

@[simp]

theorem Finset.imageOneHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [One α] [DecidableEq β] [One β] [OneHomClass F α β] (f : F) (s : Finset α) : ↑(Finset.imageOneHom f) s = Finset.image (↑f) s

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

• Finset.imageOneHom f = { toFun := Finset.image ↑f, map_one' := (_ : Finset.image (↑f) 1 = 1) }

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

• Finset.neg = { neg := Finset.image Neg.neg }

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

• Finset.inv = { inv := Finset.image Inv.inv }

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) : a⁻¹ ∈ s⁻¹

theorem Finset.card_neg_le {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} : Finset.card (-s) ≤ Finset.card s

theorem Finset.card_inv_le {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} : Finset.card s⁻¹ ≤ Finset.card s

@[simp]

theorem Finset.neg_empty {α : Type u_2} [DecidableEq α] [Neg α] : -∅ = ∅

@[simp]

theorem Finset.inv_empty {α : Type u_2} [DecidableEq α] [Inv α] : ∅⁻¹ = ∅

@[simp]

theorem Finset.neg_nonempty_iff {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} : Finset.Nonempty (-s) ↔ Finset.Nonempty s

@[simp]

theorem Finset.inv_nonempty_iff {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} : Finset.Nonempty s⁻¹ ↔ Finset.Nonempty s

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

Alias of the reverse direction of Finset.inv_nonempty_iff.

theorem Finset.Nonempty.of_inv {α : Type u_2} [DecidableEq α] [Inv α] {s : Finset α} : Finset.Nonempty s⁻¹ → Finset.Nonempty s

Alias of the forward direction of Finset.inv_nonempty_iff.

theorem Finset.Nonempty.of_neg {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} : Finset.Nonempty (-s) → Finset.Nonempty s

theorem Finset.Nonempty.neg {α : Type u_2} [DecidableEq α] [Neg α] {s : Finset α} : Finset.Nonempty s → Finset.Nonempty (-s)

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) : 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 α) : (insert a s)⁻¹ = insert a⁻¹ s⁻¹

@[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 α) : Finset.card (-s) = Finset.card s

@[simp]

theorem Finset.card_inv {α : Type u_2} [DecidableEq α] [InvolutiveInv α] (s : Finset α) : Finset.card s⁻¹ = Finset.card s

@[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

• Finset.add = { add := Finset.image₂ fun x x_1 => x + x_1 }

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

• Finset.mul = { mul := Finset.image₂ fun x x_1 => x * x_1 }

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 ∈ s → b ∈ t → a + b ∈ s + t

theorem Finset.mul_mem_mul {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} {a : α} {b : α} : a ∈ s → b ∈ t → a * b ∈ s * t

theorem Finset.card_add_le {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} : Finset.card (s + t) ≤ Finset.card s * Finset.card t

theorem Finset.card_mul_le {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} : Finset.card (s * t) ≤ Finset.card s * Finset.card t

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 α) : ∅ + s = ∅

@[simp]

theorem Finset.empty_mul {α : Type u_2} [DecidableEq α] [Mul α] (s : Finset α) : ∅ * s = ∅

@[simp]

theorem Finset.add_empty {α : Type u_2} [DecidableEq α] [Add α] (s : Finset α) : s + ∅ = ∅

@[simp]

theorem Finset.mul_empty {α : Type u_2} [DecidableEq α] [Mul α] (s : Finset α) : s * ∅ = ∅

@[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 α} : Finset.Nonempty (s + t) ↔ Finset.Nonempty s ∧ Finset.Nonempty t

@[simp]

theorem Finset.mul_nonempty {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s * t) ↔ Finset.Nonempty s ∧ Finset.Nonempty t

theorem Finset.Nonempty.add {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} : Finset.Nonempty s → Finset.Nonempty t → Finset.Nonempty (s + t)

theorem Finset.Nonempty.mul {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} : Finset.Nonempty s → Finset.Nonempty t → Finset.Nonempty (s * t)

theorem Finset.Nonempty.of_add_left {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s + t) → Finset.Nonempty s

theorem Finset.Nonempty.of_mul_left {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s * t) → Finset.Nonempty s

theorem Finset.Nonempty.of_add_right {α : Type u_2} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s + t) → Finset.Nonempty t

theorem Finset.Nonempty.of_mul_right {α : Type u_2} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s * t) → Finset.Nonempty t

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 ∈ t → x + 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 ∈ t → x * 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 + 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} [DecidableEq α] [Mul α] {u : Finset α} {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} [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}) }

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 α] : α →ₙ* Finset α

The singleton operation as a MulHom.

Equations

• Finset.singletonMulHom = { toFun := singleton, map_mul' := (_ : ∀ (x x_1 : α), {x * x_1} = {x} * {x_1}) }

@[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

• Finset.imageAddHom f = { toFun := Finset.image ↑f, map_add' := (_ : ∀ (x x_1 : Finset α), 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} [DecidableEq α] [DecidableEq β] [Add α] [Add β] [AddHomClass F α β] (f : F) (s : Finset α) : ↑(Finset.imageAddHom f) s = Finset.image (↑f) s

@[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 α) : ↑(Finset.imageMulHom f) s = Finset.image (↑f) s

def Finset.imageMulHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Mul α] [Mul β] [MulHomClass F α β] (f : F) : Finset α →ₙ* Finset β

Lift a MulHom to Finset via image.

Equations

• Finset.imageMulHom f = { toFun := Finset.image ↑f, map_mul' := (_ : ∀ (x x_1 : Finset α), Finset.image (↑f) (x * x_1) = Finset.image (↑f) x * Finset.image (↑f) x_1) }

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

• Finset.sub = { sub := Finset.image₂ fun x x_1 => x - x_1 }

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

• Finset.div = { div := Finset.image₂ fun x x_1 => x / x_1 }

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 ∈ s → b ∈ t → a - b ∈ s - t

theorem Finset.div_mem_div {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} {a : α} {b : α} : a ∈ s → b ∈ t → a / b ∈ s / t

theorem Finset.sub_card_le {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} : Finset.card (s - t) ≤ Finset.card s * Finset.card t

theorem Finset.div_card_le {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} : Finset.card (s / t) ≤ Finset.card s * Finset.card t

@[simp]

theorem Finset.empty_sub {α : Type u_2} [DecidableEq α] [Sub α] (s : Finset α) : ∅ - s = ∅

@[simp]

theorem Finset.empty_div {α : Type u_2} [DecidableEq α] [Div α] (s : Finset α) : ∅ / s = ∅

@[simp]

theorem Finset.sub_empty {α : Type u_2} [DecidableEq α] [Sub α] (s : Finset α) : s - ∅ = ∅

@[simp]

theorem Finset.div_empty {α : Type u_2} [DecidableEq α] [Div α] (s : Finset α) : s / ∅ = ∅

@[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 α} : Finset.Nonempty (s - t) ↔ Finset.Nonempty s ∧ Finset.Nonempty t

@[simp]

theorem Finset.div_nonempty {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s / t) ↔ Finset.Nonempty s ∧ Finset.Nonempty t

theorem Finset.Nonempty.sub {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} : Finset.Nonempty s → Finset.Nonempty t → Finset.Nonempty (s - t)

theorem Finset.Nonempty.div {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} : Finset.Nonempty s → Finset.Nonempty t → Finset.Nonempty (s / t)

theorem Finset.Nonempty.of_sub_left {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s - t) → Finset.Nonempty s

theorem Finset.Nonempty.of_div_left {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s / t) → Finset.Nonempty s

theorem Finset.Nonempty.of_sub_right {α : Type u_2} [DecidableEq α] [Sub α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s - t) → Finset.Nonempty t

theorem Finset.Nonempty.of_div_right {α : Type u_2} [DecidableEq α] [Div α] {s : Finset α} {t : Finset α} : Finset.Nonempty (s / t) → Finset.Nonempty t

@[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 ∈ t → x - 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 ∈ t → x / 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 - 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} [DecidableEq α] [Div α] {u : Finset α} {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'.

Instances

def Finset.nsmul {α : Type u_2} [DecidableEq α] [Zero α] [Add α] : SMul ℕ (Finset α)

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

Equations

• Finset.nsmul = { smul := nsmulRec }

def Finset.npow {α : Type u_2} [DecidableEq α] [One α] [Mul α] : Pow (Finset α) ℕ

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 }

def Finset.zsmul {α : Type u_2} [DecidableEq α] [Zero α] [Add α] [Neg α] : SMul ℤ (Finset α)

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 }

def Finset.zpow {α : Type u_2} [DecidableEq α] [One α] [Mul α] [Inv α] : Pow (Finset α) ℤ

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 }

theorem Finset.addSemigroup.proof_1 {α : Type u_1} [DecidableEq α] [AddSemigroup α] (s : Finset α) (t : Finset α) : ↑(s + t) = ↑s + ↑t

def Finset.addSemigroup {α : Type u_2} [DecidableEq α] [AddSemigroup α] : AddSemigroup (Finset α)

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

Equations

• Finset.addSemigroup = Function.Injective.addSemigroup Finset.toSet (_ : Function.Injective Finset.toSet) (_ : ∀ (s t : Finset α), ↑(s + t) = ↑s + ↑t)

def Finset.semigroup {α : Type u_2} [DecidableEq α] [Semigroup α] : Semigroup (Finset α)

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

Equations

• Finset.semigroup = Function.Injective.semigroup Finset.toSet (_ : Function.Injective Finset.toSet) (_ : ∀ (s t : Finset α), ↑(s * t) = ↑s * ↑t)

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

def Finset.addCommSemigroup {α : Type u_2} [DecidableEq α] [AddCommSemigroup α] : AddCommSemigroup (Finset α)

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

Equations

• Finset.addCommSemigroup = Function.Injective.addCommSemigroup Finset.toSet (_ : Function.Injective Finset.toSet) (_ : ∀ (s t : Finset α), ↑(s + t) = ↑s + ↑t)

def Finset.commSemigroup {α : Type u_2} [DecidableEq α] [CommSemigroup α] : CommSemigroup (Finset α)

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

Equations

• Finset.commSemigroup = Function.Injective.commSemigroup Finset.toSet (_ : Function.Injective Finset.toSet) (_ : ∀ (s t : Finset α), ↑(s * t) = ↑s * ↑t)

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}

def Finset.addZeroClass {α : Type u_2} [DecidableEq α] [AddZeroClass α] : AddZeroClass (Finset α)

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

Equations

• Finset.addZeroClass = Function.Injective.addZeroClass Finset.toSet (_ : Function.Injective Finset.toSet) (_ : ↑{0} = {0}) (_ : ∀ (s t : Finset α), ↑(s + t) = ↑s + ↑t)

def Finset.mulOneClass {α : Type u_2} [DecidableEq α] [MulOneClass α] : MulOneClass (Finset α)

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

Equations

• Finset.mulOneClass = Function.Injective.mulOneClass Finset.toSet (_ : Function.Injective Finset.toSet) (_ : ↑{1} = {1}) (_ : ∀ (s t : Finset α), ↑(s * t) = ↑s * ↑t)

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

def Finset.singletonAddMonoidHom {α : Type u_2} [DecidableEq α] [AddZeroClass α] : α →+ Finset α

The singleton operation as an AddMonoidHom.

Equations

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

def Finset.singletonMonoidHom {α : Type u_2} [DecidableEq α] [MulOneClass α] : α →* Finset α

The singleton operation as a MonoidHom.

Equations

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

@[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

theorem Finset.coeAddMonoidHom.proof_1 {α : Type u_1} [AddZeroClass α] : ↑0 = 0

noncomputable def Finset.coeAddMonoidHom {α : Type u_2} [DecidableEq α] [AddZeroClass α] : Finset α →+ Set α

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) }

noncomputable def Finset.coeMonoidHom {α : Type u_2} [DecidableEq α] [MulOneClass α] : Finset α →* Set α

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) }

@[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) : ZeroHom.toFun (Finset.imageZeroHom f) 0 = 0

def Finset.imageAddMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [AddZeroClass α] [AddZeroClass β] [AddMonoidHomClass F α β] (f : F) : Finset α →+ Finset β

Lift an add_monoid_hom to Finset via image

Equations

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

theorem Finset.imageAddMonoidHom.proof_2 {F : Type u_3} {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [AddZeroClass α] [AddZeroClass β] [AddMonoidHomClass F α β] (f : F) (x : Finset α) (y : Finset α) : AddHom.toFun (Finset.imageAddHom f) (x + y) = AddHom.toFun (Finset.imageAddHom f) x + AddHom.toFun (Finset.imageAddHom f) y

@[simp]

theorem Finset.imageAddMonoidHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [AddZeroClass α] [AddZeroClass β] [AddMonoidHomClass F α β] (f : F) : ∀ (a : Finset α), ↑(Finset.imageAddMonoidHom f) a = AddHom.toFun (Finset.imageAddHom f) a

@[simp]

theorem Finset.imageMonoidHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [MulOneClass α] [MulOneClass β] [MonoidHomClass F α β] (f : F) : ∀ (a : Finset α), ↑(Finset.imageMonoidHom f) a = MulHom.toFun (Finset.imageMulHom f) a

def Finset.imageMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [MulOneClass α] [MulOneClass β] [MonoidHomClass F α β] (f : F) : Finset α →* Finset β

Lift a MonoidHom to Finset via image.

Equations

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

@[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

def Finset.addMonoid {α : Type u_2} [DecidableEq α] [AddMonoid α] : AddMonoid (Finset α)

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

Equations

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

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 α] : Monoid (Finset α)

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

Equations

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

abbrev Finset.nsmul_mem_nsmul.match_1 (motive : ℕ → Prop) : (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive (Nat.succ n)) → motive x

Equations

• Finset.nsmul_mem_nsmul.match_1 motive x h_1 h_2 = Nat.casesOn x (h_1 ()) fun n => h_2 n

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 ≤ n → m • s ⊆ n • s

theorem Finset.pow_subset_pow_of_one_mem {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {m : ℕ} {n : ℕ} (hs : 1 ∈ s) : m ≤ n → s ^ 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 n → Finset α} : 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 n → Finset α} : 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) : n • ∅ = ∅

@[simp]

theorem Finset.empty_pow {α : Type u_2} [DecidableEq α] [Monoid α] {n : ℕ} (hn : n ≠ 0) : ∅ ^ n = ∅

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 : α} : IsAddUnit a → IsAddUnit {a}

theorem IsUnit.finset {α : Type u_2} [DecidableEq α] [Monoid α] {a : α} : IsUnit a → IsUnit {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

def Finset.addCommMonoid {α : Type u_2} [DecidableEq α] [AddCommMonoid α] : AddCommMonoid (Finset α)

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

Equations

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

def Finset.commMonoid {α : Type u_2} [DecidableEq α] [CommMonoid α] : CommMonoid (Finset α)

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

Equations

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

@[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

• Finset.coe_zsmul.match_1 motive x h_1 h_2 = Int.casesOn x (fun a => h_1 a) fun a => h_2 a

@[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

def Finset.subtractionMonoid {α : Type u_2} [DecidableEq α] [SubtractionMonoid α] : SubtractionMonoid (Finset α)

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

Equations

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

theorem Finset.subtractionMonoid.proof_1 {α : Type u_1} [SubtractionMonoid α] : ↑0 = 0

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

def Finset.divisionMonoid {α : Type u_2} [DecidableEq α] [DivisionMonoid α] : DivisionMonoid (Finset α)

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

Equations

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

@[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 α} : IsAddUnit ↑s ↔ IsAddUnit s

@[simp]

theorem Finset.isUnit_coe {α : Type u_2} [DecidableEq α] [DivisionMonoid α] {s : Finset α} : IsUnit ↑s ↔ IsUnit s

theorem Finset.subtractionCommMonoid.proof_1 {α : Type u_1} [SubtractionCommMonoid α] : ↑0 = 0

theorem Finset.subtractionCommMonoid.proof_6 {α : Type u_1} [DecidableEq α] [SubtractionCommMonoid α] (s : Finset α) (n : ℤ) : ↑(n • s) = n • ↑s

theorem Finset.subtractionCommMonoid.proof_3 {α : Type u_1} [DecidableEq α] [SubtractionCommMonoid α] (s : Finset α) : ↑(-s) = -↑s

theorem Finset.subtractionCommMonoid.proof_4 {α : Type u_1} [DecidableEq α] [SubtractionCommMonoid α] (s : Finset α) (t : Finset α) : ↑(s - t) = ↑s - ↑t

def Finset.subtractionCommMonoid {α : Type u_2} [DecidableEq α] [SubtractionCommMonoid α] : SubtractionCommMonoid (Finset α)

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

Equations

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

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

def Finset.divisionCommMonoid {α : Type u_2} [DecidableEq α] [DivisionCommMonoid α] : DivisionCommMonoid (Finset α)

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

Equations

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

def Finset.distribNeg {α : Type u_2} [DecidableEq α] [Mul α] [HasDistribNeg α] : HasDistribNeg (Finset α)

Finset α has distributive negation if α has.

Equations

• Finset.distribNeg = Function.Injective.hasDistribNeg Finset.toSet (_ : Function.Injective Finset.toSet) (_ : ∀ (s : Finset α), ↑(-s) = -↑s) (_ : ∀ (s t : Finset α), ↑(s * t) = ↑s * ↑t)

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 s → Prop) : (h : Finset.Nonempty s) → ((a : α) → (ha : a ∈ s) → motive (_ : ∃ x, x ∈ s)) → motive h

Equations

• Finset.Nonempty.zero_mem_sub.match_1 motive h h_1 = Exists.casesOn h fun w h => h_1 w h

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 : α) : IsAddUnit {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

• Finset.vadd = { vadd := Finset.image₂ fun x x_1 => x +ᵥ x_1 }

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

• Finset.smul = { smul := Finset.image₂ fun x x_1 => x • x_1 }

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 ∈ s → b ∈ t → a +ᵥ b ∈ s +ᵥ t

theorem Finset.smul_mem_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} {a : α} {b : β} : a ∈ s → b ∈ t → a • b ∈ s • t

theorem Finset.vadd_card_le {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} : Finset.card (s +ᵥ t) ≤ Finset.card s • Finset.card t

theorem Finset.smul_card_le {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} : Finset.card (s • t) ≤ Finset.card s • Finset.card t

@[simp]

theorem Finset.empty_vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (t : Finset β) : ∅ +ᵥ t = ∅

@[simp]

theorem Finset.empty_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (t : Finset β) : ∅ • t = ∅

@[simp]

theorem Finset.vadd_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (s : Finset α) : s +ᵥ ∅ = ∅

@[simp]

theorem Finset.smul_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (s : Finset α) : s • ∅ = ∅

@[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 β} : Finset.Nonempty (s +ᵥ t) ↔ Finset.Nonempty s ∧ Finset.Nonempty t

@[simp]

theorem Finset.smul_nonempty_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} : Finset.Nonempty (s • t) ↔ Finset.Nonempty s ∧ Finset.Nonempty t

theorem Finset.Nonempty.vadd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} : Finset.Nonempty s → Finset.Nonempty t → Finset.Nonempty (s +ᵥ t)

theorem Finset.Nonempty.smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} : Finset.Nonempty s → Finset.Nonempty t → Finset.Nonempty (s • t)

theorem Finset.Nonempty.of_vadd_left {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} : Finset.Nonempty (s +ᵥ t) → Finset.Nonempty s

theorem Finset.Nonempty.of_smul_left {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} : Finset.Nonempty (s • t) → Finset.Nonempty s

theorem Finset.Nonempty.of_vadd_right {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset α} {t : Finset β} : Finset.Nonempty (s +ᵥ t) → Finset.Nonempty t

theorem Finset.Nonempty.of_smul_right {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset α} {t : Finset β} : Finset.Nonempty (s • t) → Finset.Nonempty t

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 ∈ t → a +ᵥ 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 ∈ t → a • 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 +ᵥ t → ∃ s' 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 • t → ∃ s' 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

• Finset.vsub = { vsub := Finset.image₂ fun x x_1 => x -ᵥ x_1 }

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 ∈ s → c ∈ t → b -ᵥ c ∈ s -ᵥ t

theorem Finset.vsub_card_le {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t : Finset β} : Finset.card (s -ᵥ t) ≤ Finset.card s * Finset.card t

@[simp]

theorem Finset.empty_vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] (t : Finset β) : ∅ -ᵥ t = ∅

@[simp]

theorem Finset.vsub_empty {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] (s : Finset β) : s -ᵥ ∅ = ∅

@[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 β} : Finset.Nonempty (s -ᵥ t) ↔ Finset.Nonempty s ∧ Finset.Nonempty t

theorem Finset.Nonempty.vsub {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t : Finset β} : Finset.Nonempty s → Finset.Nonempty t → Finset.Nonempty (s -ᵥ t)

theorem Finset.Nonempty.of_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t : Finset β} : Finset.Nonempty (s -ᵥ t) → Finset.Nonempty s

theorem Finset.Nonempty.of_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] [DecidableEq α] {s : Finset β} {t : Finset β} : Finset.Nonempty (s -ᵥ t) → Finset.Nonempty t

@[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 ∈ t → x -ᵥ 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 -ᵥ t → ∃ s' 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

• Finset.vaddFinset = { vadd := fun a => Finset.image ((fun x x_1 => x +ᵥ x_1) a) }

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) }

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 ∈ s → a +ᵥ b ∈ a +ᵥ s

theorem Finset.smul_mem_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} {b : β} : b ∈ s → a • b ∈ a • s

theorem Finset.vadd_finset_card_le {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} : Finset.card (a +ᵥ s) ≤ Finset.card s

theorem Finset.smul_finset_card_le {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} : Finset.card (a • s) ≤ Finset.card s

@[simp]

theorem Finset.vadd_finset_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (a : α) : a +ᵥ ∅ = ∅

@[simp]

theorem Finset.smul_finset_empty {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (a : α) : 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 : α} : Finset.Nonempty (a +ᵥ s) ↔ Finset.Nonempty s

@[simp]

theorem Finset.smul_finset_nonempty {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} : Finset.Nonempty (a • s) ↔ Finset.Nonempty s

theorem Finset.Nonempty.vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] {s : Finset β} {a : α} (hs : Finset.Nonempty s) : Finset.Nonempty (a +ᵥ s)

theorem Finset.Nonempty.smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {a : α} (hs : Finset.Nonempty s) : Finset.Nonempty (a • 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 ⊆ t → a +ᵥ s ⊆ a +ᵥ t

theorem Finset.smul_finset_subset_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {s : Finset β} {t : Finset β} {a : α} : s ⊆ t → a • 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 ∈ s → a +ᵥ t ⊆ s +ᵥ t

theorem Finset.smul_finset_subset_smul {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] {t : Finset β} {a : α} {s : Finset α} : a ∈ s → a • 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 α β γ] : VAddCommClass α β (Finset γ)

instance Finset.vaddCommClass_finset {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass α β (Finset γ)

Equations

• @Finset.vaddCommClass_finset = @Finset.vaddCommClass_finset.proof_1

instance Finset.smulCommClass_finset {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α β (Finset γ)

Equations

• @Finset.smulCommClass_finset = @Finset.smulCommClass_finset.proof_1

theorem Finset.vaddCommClass_finset'.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass α (Finset β) (Finset γ)

instance Finset.vaddCommClass_finset' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass α (Finset β) (Finset γ)

Equations

• @Finset.vaddCommClass_finset' = @Finset.vaddCommClass_finset'.proof_1

instance Finset.smulCommClass_finset' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α (Finset β) (Finset γ)

Equations

• @Finset.smulCommClass_finset' = @Finset.smulCommClass_finset'.proof_1

theorem Finset.vaddCommClass_finset''.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass (Finset α) β (Finset γ)

instance Finset.vaddCommClass_finset'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass (Finset α) β (Finset γ)

Equations

• @Finset.vaddCommClass_finset'' = @Finset.vaddCommClass_finset''.proof_1

instance Finset.smulCommClass_finset'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass (Finset α) β (Finset γ)

Equations

• @Finset.smulCommClass_finset'' = @Finset.smulCommClass_finset''.proof_1

instance Finset.vaddCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass (Finset α) (Finset β) (Finset γ)

Equations

• @Finset.vaddCommClass = @Finset.vaddCommClass.proof_1

theorem Finset.vaddCommClass.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass (Finset α) (Finset β) (Finset γ)

instance Finset.smulCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass (Finset α) (Finset β) (Finset γ)

Equations

• @Finset.smulCommClass = @Finset.smulCommClass.proof_1

theorem Finset.vaddAssocClass.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq γ] [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass α β (Finset γ)

instance Finset.vaddAssocClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass α β (Finset γ)

Equations

• @Finset.vaddAssocClass = @Finset.vaddAssocClass.proof_1

instance Finset.isScalarTower {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α β (Finset γ)

Equations

• @Finset.isScalarTower = @Finset.isScalarTower.proof_1

theorem Finset.vaddAssocClass'.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq γ] [DecidableEq β] [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass α (Finset β) (Finset γ)

instance Finset.vaddAssocClass' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [DecidableEq β] [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass α (Finset β) (Finset γ)

Equations

• @Finset.vaddAssocClass' = @Finset.vaddAssocClass'.proof_1

instance Finset.isScalarTower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [DecidableEq β] [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α (Finset β) (Finset γ)

Equations

• @Finset.isScalarTower' = @Finset.isScalarTower'.proof_1

theorem Finset.vaddAssocClass''.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq γ] [DecidableEq β] [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass (Finset α) (Finset β) (Finset γ)

instance Finset.vaddAssocClass'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [DecidableEq β] [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass (Finset α) (Finset β) (Finset γ)

Equations

• @Finset.vaddAssocClass'' = @Finset.vaddAssocClass''.proof_1

instance Finset.isScalarTower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [DecidableEq β] [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower (Finset α) (Finset β) (Finset γ)

Equations

• @Finset.isScalarTower'' = @Finset.isScalarTower''.proof_1

theorem Finset.isCentralVAdd.proof_1 {α : Type u_1} {β : Type u_2} [DecidableEq β] [VAdd α β] [VAdd αᵃᵒᵖ β] [IsCentralVAdd α β] : IsCentralVAdd α (Finset β)

instance Finset.isCentralVAdd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] [VAdd αᵃᵒᵖ β] [IsCentralVAdd α β] : IsCentralVAdd α (Finset β)

Equations

• @Finset.isCentralVAdd = @Finset.isCentralVAdd.proof_1

instance Finset.isCentralScalar {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α β] : IsCentralScalar α (Finset β)

Equations

• @Finset.isCentralScalar = @Finset.isCentralScalar.proof_1

def Finset.addAction {α : Type u_2} {β : Type u_3} [DecidableEq β] [DecidableEq α] [AddMonoid α] [AddAction α β] : AddAction (Finset α) (Finset β)

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.

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 α β] : MulAction (Finset α) (Finset β)

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.

def Finset.addActionFinset {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddMonoid α] [AddAction α β] : AddAction α (Finset β)

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

Equations

• Finset.addActionFinset = Function.Injective.addAction Finset.toSet (_ : Function.Injective Finset.toSet) (_ : ∀ (a : α) (s : Finset β), ↑(a +ᵥ s) = a +ᵥ ↑s)

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 α β] : MulAction α (Finset β)

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

Equations

• Finset.mulActionFinset = Function.Injective.mulAction Finset.toSet (_ : Function.Injective Finset.toSet) (_ : ∀ (a : α) (s : Finset β), ↑(a • s) = a • ↑s)

def Finset.distribMulActionFinset {α : Type u_2} {β : Type u_3} [DecidableEq β] [Monoid α] [AddMonoid β] [DistribMulAction α β] : DistribMulAction α (Finset β)

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

Equations

• Finset.distribMulActionFinset = Function.Injective.distribMulAction Finset.coeAddMonoidHom (_ : Function.Injective Finset.toSet) (_ : ∀ (a : α) (s : Finset β), ↑(a • s) = a • ↑s)

def Finset.mulDistribMulActionFinset {α : Type u_2} {β : Type u_3} [DecidableEq β] [Monoid α] [Monoid β] [MulDistribMulAction α β] : MulDistribMulAction α (Finset β)

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

Equations

• Finset.mulDistribMulActionFinset = Function.Injective.mulDistribMulAction Finset.coeMonoidHom (_ : Function.Injective Finset.toSet) (_ : ∀ (a : α) (s : Finset β), ↑(a • s) = a • ↑s)

instance Finset.instNoZeroDivisorsFinsetMulZero {α : Type u_2} [DecidableEq α] [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors (Finset α)

Equations

• @Finset.instNoZeroDivisorsFinsetMulZero = @Finset.instNoZeroDivisorsFinsetMulZero.proof_1

instance Finset.noZeroSMulDivisors {α : Type u_2} {β : Type u_3} [DecidableEq β] [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors (Finset α) (Finset β)

Equations

• @Finset.noZeroSMulDivisors = @Finset.noZeroSMulDivisors.proof_1

instance Finset.noZeroSMulDivisors_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors α (Finset β)

Equations

• @Finset.noZeroSMulDivisors_finset = @Finset.noZeroSMulDivisors_finset.proof_1

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)) : AddOpposite.op a +ᵥ s +ᵥ t = s +ᵥ (a +ᵥ t)

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 ∈ t → AddOpposite.op a +ᵥ s ⊆ s + t

theorem Finset.op_smul_finset_subset_mul {α : Type u_2} [Mul α] [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} : a ∈ t → MulOpposite.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 ∈ s → a +ᵥ t ⊆ u

theorem Finset.mul_subset_iff_left {α : Type u_2} [Mul α] [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} : s * t ⊆ u ↔ ∀ (a : α), a ∈ s → a • t ⊆ u

theorem Finset.add_subset_iff_right {α : Type u_2} [Add α] [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} : s + t ⊆ u ↔ ∀ (b : α), b ∈ t → AddOpposite.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 ∈ t → MulOpposite.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 : α) : Finset.card ({a} + t) = Finset.card t

@[simp]

theorem Finset.card_singleton_mul {α : Type u_2} [LeftCancelSemigroup α] [DecidableEq α] (t : Finset α) (a : α) : Finset.card ({a} * t) = Finset.card t

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)

theorem Finset.card_le_card_add_left {α : Type u_2} [AddLeftCancelSemigroup α] [DecidableEq α] (t : Finset α) {s : Finset α} (hs : Finset.Nonempty s) : Finset.card t ≤ Finset.card (s + t)

theorem Finset.card_le_card_mul_left {α : Type u_2} [LeftCancelSemigroup α] [DecidableEq α] (t : Finset α) {s : Finset α} (hs : Finset.Nonempty s) : Finset.card t ≤ Finset.card (s * t)

@[simp]

theorem Finset.card_add_singleton {α : Type u_2} [AddRightCancelSemigroup α] [DecidableEq α] (s : Finset α) (a : α) : Finset.card (s + {a}) = Finset.card s

@[simp]

theorem Finset.card_mul_singleton {α : Type u_2} [RightCancelSemigroup α] [DecidableEq α] (s : Finset α) (a : α) : Finset.card (s * {a}) = Finset.card s

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.card_le_card_add_right {α : Type u_2} [AddRightCancelSemigroup α] [DecidableEq α] (s : Finset α) {t : Finset α} (ht : Finset.Nonempty t) : Finset.card s ≤ Finset.card (s + t)

theorem Finset.card_le_card_mul_right {α : Type u_2} [RightCancelSemigroup α] [DecidableEq α] (s : Finset α) {t : Finset α} (ht : Finset.Nonempty t) : Finset.card s ≤ Finset.card (s * t)

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 β) : Finset.card (a +ᵥ s) = Finset.card s

@[simp]

theorem Finset.card_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] (a : α) (s : Finset β) : Finset.card (a • s) = Finset.card s

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) id → Finset.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) id → Finset.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) id → Finset.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) id → Finset.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) id → Finset.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) id → Finset.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 α β] : 0 ∈ s • t ↔ 0 ∈ s ∧ Finset.Nonempty t ∨ 0 ∈ t ∧ Finset.Nonempty s

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 α] : Set.toFinset 0 = 0

@[simp]

theorem Set.toFinset_one {α : Type u_2} [One α] : Set.toFinset 1 = 1

@[simp]

theorem Set.Finite.toFinset_zero {α : Type u_2} [Zero α] (h : optParam (Set.Finite 0) (_ : Set.Finite 0)) : Set.Finite.toFinset h = 0

@[simp]

theorem Set.Finite.toFinset_one {α : Type u_2} [One α] (h : optParam (Set.Finite 1) (_ : Set.Finite 1)) : Set.Finite.toFinset h = 1

@[simp]

theorem Set.toFinset_add {α : Type u_2} [DecidableEq α] [Add α] (s : Set α) (t : Set α) [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s + t)] : Set.toFinset (s + t) = Set.toFinset s + Set.toFinset t

@[simp]

theorem Set.toFinset_mul {α : Type u_2} [DecidableEq α] [Mul α] (s : Set α) (t : Set α) [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s * t)] : Set.toFinset (s * t) = Set.toFinset s * Set.toFinset 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))) : Set.Finite.toFinset hf = Set.Finite.toFinset hs + Set.Finite.toFinset ht

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))) : Set.Finite.toFinset hf = Set.Finite.toFinset hs * Set.Finite.toFinset ht

@[simp]

theorem Set.toFinset_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] [DecidableEq β] (s : Set α) (t : Set β) [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s +ᵥ t)] : Set.toFinset (s +ᵥ t) = Set.toFinset s +ᵥ Set.toFinset 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)] : Set.toFinset (s • t) = Set.toFinset s • Set.toFinset 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))) : Set.Finite.toFinset hf = Set.Finite.toFinset hs +ᵥ Set.Finite.toFinset ht

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))) : Set.Finite.toFinset hf = Set.Finite.toFinset hs • Set.Finite.toFinset ht

@[simp]

theorem Set.toFinset_vadd_set {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] (a : α) (s : Set β) [Fintype ↑s] [Fintype ↑(a +ᵥ s)] : Set.toFinset (a +ᵥ s) = a +ᵥ Set.toFinset s

@[simp]

theorem Set.toFinset_smul_set {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] (a : α) (s : Set β) [Fintype ↑s] [Fintype ↑(a • s)] : Set.toFinset (a • s) = a • Set.toFinset 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))) : Set.Finite.toFinset hf = a +ᵥ Set.Finite.toFinset hs

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))) : Set.Finite.toFinset hf = a • Set.Finite.toFinset hs

@[simp]

theorem Set.toFinset_vsub {α : Type u_2} {β : Type u_3} [DecidableEq α] [VSub α β] (s : Set β) (t : Set β) [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s -ᵥ t)] : Set.toFinset (s -ᵥ t) = Set.toFinset s -ᵥ Set.toFinset 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))) : Set.Finite.toFinset hf = Set.Finite.toFinset hs -ᵥ Set.Finite.toFinset ht