mathlib documentation

data.finset.pointwise

Pointwise operations of finsets #

This file defines pointwise algebraic operations on finsets.

Main declarations #

For finsets s and t:

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

Implementation notes #

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

Tags #

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

0/1 as finsets #

@[protected]
def finset.has_one {α : Type u_2} [has_one α] :

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

Equations
@[protected]
def finset.has_zero {α : Type u_2} [has_zero α] :

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

Equations
@[simp]
theorem finset.mem_one {α : Type u_2} [has_one α] {a : α} :
a 1 a = 1
@[simp]
theorem finset.mem_zero {α : Type u_2} [has_zero α] {a : α} :
a 0 a = 0
@[simp, norm_cast]
theorem finset.coe_zero {α : Type u_2} [has_zero α] :
0 = 0
@[simp, norm_cast]
theorem finset.coe_one {α : Type u_2} [has_one α] :
1 = 1
@[simp]
theorem finset.zero_subset {α : Type u_2} [has_zero α] {s : finset α} :
0 s 0 s
@[simp]
theorem finset.one_subset {α : Type u_2} [has_one α] {s : finset α} :
1 s 1 s
theorem finset.singleton_one {α : Type u_2} [has_one α] :
{1} = 1
theorem finset.singleton_zero {α : Type u_2} [has_zero α] :
{0} = 0
theorem finset.one_mem_one {α : Type u_2} [has_one α] :
1 1
theorem finset.zero_mem_zero {α : Type u_2} [has_zero α] :
0 0
theorem finset.one_nonempty {α : Type u_2} [has_one α] :
theorem finset.zero_nonempty {α : Type u_2} [has_zero α] :
@[protected, simp]
theorem finset.map_zero {α : Type u_2} {β : Type u_3} [has_zero α] {f : α β} :
finset.map f 0 = {f 0}
@[protected, simp]
theorem finset.map_one {α : Type u_2} {β : Type u_3} [has_one α] {f : α β} :
finset.map f 1 = {f 1}
@[simp]
theorem finset.image_zero {α : Type u_2} {β : Type u_3} [has_zero α] [decidable_eq β] {f : α → β} :
finset.image f 0 = {f 0}
@[simp]
theorem finset.image_one {α : Type u_2} {β : Type u_3} [has_one α] [decidable_eq β] {f : α → β} :
finset.image f 1 = {f 1}
theorem finset.subset_one_iff_eq {α : Type u_2} [has_one α] {s : finset α} :
s 1 s = s = 1
theorem finset.subset_zero_iff_eq {α : Type u_2} [has_zero α] {s : finset α} :
s 0 s = s = 0
theorem finset.nonempty.subset_one_iff {α : Type u_2} [has_one α] {s : finset α} (h : s.nonempty) :
s 1 s = 1
theorem finset.nonempty.subset_zero_iff {α : Type u_2} [has_zero α] {s : finset α} (h : s.nonempty) :
s 0 s = 0
def finset.singleton_zero_hom {α : Type u_2} [has_zero α] :

The singleton operation as a zero_hom.

Equations
def finset.singleton_one_hom {α : Type u_2} [has_one α] :
one_hom α (finset α)

The singleton operation as a one_hom.

Equations
@[simp]
theorem finset.singleton_zero_hom_apply {α : Type u_2} [has_zero α] (a : α) :
@[simp]
theorem finset.singleton_one_hom_apply {α : Type u_2} [has_one α] (a : α) :

Finset negation/inversion #

@[protected]
def finset.has_inv {α : Type u_2} [decidable_eq α] [has_inv α] :

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

Equations
@[protected]
def finset.has_neg {α : Type u_2} [decidable_eq α] [has_neg α] :

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

Equations
theorem finset.inv_def {α : Type u_2} [decidable_eq α] [has_inv α] {s : finset α} :
s⁻¹ = finset.image (λ (x : α), x⁻¹) s
theorem finset.neg_def {α : Type u_2} [decidable_eq α] [has_neg α] {s : finset α} :
-s = finset.image (λ (x : α), -x) s
theorem finset.image_inv {α : Type u_2} [decidable_eq α] [has_inv α] {s : finset α} :
finset.image (λ (x : α), x⁻¹) s = s⁻¹
theorem finset.image_neg {α : Type u_2} [decidable_eq α] [has_neg α] {s : finset α} :
finset.image (λ (x : α), -x) s = -s
theorem finset.mem_neg {α : Type u_2} [decidable_eq α] [has_neg α] {s : finset α} {x : α} :
x -s ∃ (y : α) (H : y s), -y = x
theorem finset.mem_inv {α : Type u_2} [decidable_eq α] [has_inv α] {s : finset α} {x : α} :
x s⁻¹ ∃ (y : α) (H : y s), y⁻¹ = x
theorem finset.neg_mem_neg {α : Type u_2} [decidable_eq α] [has_neg α] {s : finset α} {a : α} (ha : a s) :
-a -s
theorem finset.inv_mem_inv {α : Type u_2} [decidable_eq α] [has_inv α] {s : finset α} {a : α} (ha : a s) :
theorem finset.card_inv_le {α : Type u_2} [decidable_eq α] [has_inv α] {s : finset α} :
theorem finset.card_neg_le {α : Type u_2} [decidable_eq α] [has_neg α] {s : finset α} :
(-s).card s.card
@[simp]
theorem finset.inv_empty {α : Type u_2} [decidable_eq α] [has_inv α] :
@[simp]
theorem finset.neg_empty {α : Type u_2} [decidable_eq α] [has_neg α] :
@[simp]
theorem finset.neg_nonempty_iff {α : Type u_2} [decidable_eq α] [has_neg α] {s : finset α} :
@[simp]
theorem finset.inv_nonempty_iff {α : Type u_2} [decidable_eq α] [has_inv α] {s : finset α} :
theorem finset.nonempty.of_inv {α : Type u_2} [decidable_eq α] [has_inv α] {s : finset α} :

Alias of the reverse direction of finset.inv_nonempty_iff.

theorem finset.nonempty.inv {α : Type u_2} [decidable_eq α] [has_inv α] {s : finset α} :

Alias of the forward direction of finset.inv_nonempty_iff.

theorem finset.inv_subset_inv {α : Type u_2} [decidable_eq α] [has_inv α] {s t : finset α} (h : s t) :
theorem finset.neg_subset_neg {α : Type u_2} [decidable_eq α] [has_neg α] {s t : finset α} (h : s t) :
-s -t
@[simp]
theorem finset.inv_singleton {α : Type u_2} [decidable_eq α] [has_inv α] (a : α) :
{a}⁻¹ = {a⁻¹}
@[simp]
theorem finset.neg_singleton {α : Type u_2} [decidable_eq α] [has_neg α] (a : α) :
-{a} = {-a}
@[simp, norm_cast]
theorem finset.coe_neg {α : Type u_2} [decidable_eq α] [has_involutive_neg α] (s : finset α) :
@[simp, norm_cast]
theorem finset.coe_inv {α : Type u_2} [decidable_eq α] [has_involutive_inv α] (s : finset α) :
@[simp]
theorem finset.card_inv {α : Type u_2} [decidable_eq α] [has_involutive_inv α] (s : finset α) :
@[simp]
theorem finset.card_neg {α : Type u_2} [decidable_eq α] [has_involutive_neg α] (s : finset α) :
(-s).card = s.card
@[simp]
theorem finset.preimage_neg {α : Type u_2} [decidable_eq α] [has_involutive_neg α] (s : finset α) :
@[simp]
theorem finset.preimage_inv {α : Type u_2} [decidable_eq α] [has_involutive_inv α] (s : finset α) :

Finset addition/multiplication #

@[protected]
def finset.has_add {α : Type u_2} [decidable_eq α] [has_add α] :

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

Equations
@[protected]
def finset.has_mul {α : Type u_2} [decidable_eq α] [has_mul α] :

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

Equations
theorem finset.add_def {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
s + t = finset.image (λ (p : α × α), p.fst + p.snd) (s ×ˢ t)
theorem finset.mul_def {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
s * t = finset.image (λ (p : α × α), p.fst * p.snd) (s ×ˢ t)
theorem finset.image_mul_product {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
finset.image (λ (x : α × α), x.fst * x.snd) (s ×ˢ t) = s * t
theorem finset.image_add_product {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
finset.image (λ (x : α × α), x.fst + x.snd) (s ×ˢ t) = s + t
theorem finset.mem_mul {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} {x : α} :
x s * t ∃ (y z : α), y s z t y * z = x
theorem finset.mem_add {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} {x : α} :
x s + t ∃ (y z : α), y s z t y + z = x
@[simp, norm_cast]
theorem finset.coe_add {α : Type u_2} [decidable_eq α] [has_add α] (s t : finset α) :
(s + t) = s + t
@[simp, norm_cast]
theorem finset.coe_mul {α : Type u_2} [decidable_eq α] [has_mul α] (s t : finset α) :
(s * t) = s * t
theorem finset.mul_mem_mul {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} {a b : α} :
a sb ta * b s * t
theorem finset.add_mem_add {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} {a b : α} :
a sb ta + b s + t
theorem finset.card_add_le {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
(s + t).card s.card * t.card
theorem finset.card_mul_le {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
(s * t).card s.card * t.card
theorem finset.card_mul_iff {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
(s * t).card = s.card * t.card set.inj_on (λ (p : α × α), p.fst * p.snd) (s ×ˢ t)
theorem finset.card_add_iff {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
(s + t).card = s.card * t.card set.inj_on (λ (p : α × α), p.fst + p.snd) (s ×ˢ t)
@[simp]
theorem finset.empty_mul {α : Type u_2} [decidable_eq α] [has_mul α] (s : finset α) :
@[simp]
theorem finset.empty_add {α : Type u_2} [decidable_eq α] [has_add α] (s : finset α) :
@[simp]
theorem finset.add_empty {α : Type u_2} [decidable_eq α] [has_add α] (s : finset α) :
@[simp]
theorem finset.mul_empty {α : Type u_2} [decidable_eq α] [has_mul α] (s : finset α) :
@[simp]
theorem finset.mul_eq_empty {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
s * t = s = t =
@[simp]
theorem finset.add_eq_empty {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
s + t = s = t =
@[simp]
theorem finset.add_nonempty {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
@[simp]
theorem finset.mul_nonempty {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
theorem finset.nonempty.mul {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
s.nonemptyt.nonempty(s * t).nonempty
theorem finset.nonempty.add {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
s.nonemptyt.nonempty(s + t).nonempty
theorem finset.nonempty.of_mul_left {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
(s * t).nonempty → s.nonempty
theorem finset.nonempty.of_add_left {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
(s + t).nonempty → s.nonempty
theorem finset.nonempty.of_add_right {α : Type u_2} [decidable_eq α] [has_add α] {s t : finset α} :
(s + t).nonempty → t.nonempty
theorem finset.nonempty.of_mul_right {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
(s * t).nonempty → t.nonempty
theorem finset.mul_singleton {α : Type u_2} [decidable_eq α] [has_mul α] {s : finset α} (a : α) :
s * {a} = finset.image (λ (_x : α), _x * a) s
theorem finset.add_singleton {α : Type u_2} [decidable_eq α] [has_add α] {s : finset α} (a : α) :
s + {a} = finset.image (λ (_x : α), _x + a) s
theorem finset.singleton_add {α : Type u_2} [decidable_eq α] [has_add α] {s : finset α} (a : α) :
theorem finset.singleton_mul {α : Type u_2} [decidable_eq α] [has_mul α] {s : finset α} (a : α) :
@[simp]
theorem finset.singleton_add_singleton {α : Type u_2} [decidable_eq α] [has_add α] (a b : α) :
{a} + {b} = {a + b}
@[simp]
theorem finset.singleton_mul_singleton {α : Type u_2} [decidable_eq α] [has_mul α] (a b : α) :
{a} * {b} = {a * b}
theorem finset.add_subset_add {α : Type u_2} [decidable_eq α] [has_add α] {s₁ s₂ t₁ t₂ : finset α} :
s₁ s₂t₁ t₂s₁ + t₁ s₂ + t₂
theorem finset.mul_subset_mul {α : Type u_2} [decidable_eq α] [has_mul α] {s₁ s₂ t₁ t₂ : finset α} :
s₁ s₂t₁ t₂s₁ * t₁ s₂ * t₂
theorem finset.add_subset_add_left {α : Type u_2} [decidable_eq α] [has_add α] {s t₁ t₂ : finset α} :
t₁ t₂s + t₁ s + t₂
theorem finset.mul_subset_mul_left {α : Type u_2} [decidable_eq α] [has_mul α] {s t₁ t₂ : finset α} :
t₁ t₂s * t₁ s * t₂
theorem finset.add_subset_add_right {α : Type u_2} [decidable_eq α] [has_add α] {s₁ s₂ t : finset α} :
s₁ s₂s₁ + t s₂ + t
theorem finset.mul_subset_mul_right {α : Type u_2} [decidable_eq α] [has_mul α] {s₁ s₂ t : finset α} :
s₁ s₂s₁ * t s₂ * t
theorem finset.add_subset_iff {α : Type u_2} [decidable_eq α] [has_add α] {s t u : finset α} :
s + t u ∀ (x : α), x s∀ (y : α), y tx + y u
theorem finset.mul_subset_iff {α : Type u_2} [decidable_eq α] [has_mul α] {s t u : finset α} :
s * t u ∀ (x : α), x s∀ (y : α), y tx * y u
theorem finset.union_mul {α : Type u_2} [decidable_eq α] [has_mul α] {s₁ s₂ t : finset α} :
(s₁ s₂) * t = s₁ * t s₂ * t
theorem finset.union_add {α : Type u_2} [decidable_eq α] [has_add α] {s₁ s₂ t : finset α} :
s₁ s₂ + t = s₁ + t (s₂ + t)
theorem finset.add_union {α : Type u_2} [decidable_eq α] [has_add α] {s t₁ t₂ : finset α} :
s + (t₁ t₂) = s + t₁ (s + t₂)
theorem finset.mul_union {α : Type u_2} [decidable_eq α] [has_mul α] {s t₁ t₂ : finset α} :
s * (t₁ t₂) = s * t₁ s * t₂
theorem finset.inter_mul_subset {α : Type u_2} [decidable_eq α] [has_mul α] {s₁ s₂ t : finset α} :
s₁ s₂ * t s₁ * t (s₂ * t)
theorem finset.inter_add_subset {α : Type u_2} [decidable_eq α] [has_add α] {s₁ s₂ t : finset α} :
s₁ s₂ + t (s₁ + t) (s₂ + t)
theorem finset.add_inter_subset {α : Type u_2} [decidable_eq α] [has_add α] {s t₁ t₂ : finset α} :
s + t₁ t₂ (s + t₁) (s + t₂)
theorem finset.mul_inter_subset {α : Type u_2} [decidable_eq α] [has_mul α] {s t₁ t₂ : finset α} :
s * (t₁ t₂) s * t₁ (s * t₂)
theorem finset.subset_mul {α : Type u_2} [decidable_eq α] [has_mul α] {u : finset α} {s t : set α} :
u s * t(∃ (s' t' : finset α), 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.subset_add {α : Type u_2} [decidable_eq α] [has_add α] {u : finset α} {s t : set α} :
u s + t(∃ (s' t' : finset α), 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.image_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [decidable_eq α] [decidable_eq β] [has_add α] [has_add β] [add_hom_class F α β] (m : F) {s t : finset α} :
theorem finset.image_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [decidable_eq α] [decidable_eq β] [has_mul α] [has_mul β] [mul_hom_class F α β] (m : F) {s t : finset α} :
def finset.singleton_add_hom {α : Type u_2} [decidable_eq α] [has_add α] :
add_hom α (finset α)

The singleton operation as an add_hom.

Equations
def finset.singleton_mul_hom {α : Type u_2} [decidable_eq α] [has_mul α] :

The singleton operation as a mul_hom.

Equations
@[simp]
theorem finset.singleton_mul_hom_apply {α : Type u_2} [decidable_eq α] [has_mul α] (a : α) :
@[simp]
theorem finset.singleton_add_hom_apply {α : Type u_2} [decidable_eq α] [has_add α] (a : α) :

Finset subtraction/division #

@[protected]
def finset.has_sub {α : Type u_2} [decidable_eq α] [has_sub α] :

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

Equations
@[protected]
def finset.has_div {α : Type u_2} [decidable_eq α] [has_div α] :

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

Equations
theorem finset.div_def {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} :
s / t = finset.image (λ (p : α × α), p.fst / p.snd) (s ×ˢ t)
theorem finset.sub_def {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} :
s - t = finset.image (λ (p : α × α), p.fst - p.snd) (s ×ˢ t)
theorem finset.image_div_prod {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} :
finset.image (λ (x : α × α), x.fst / x.snd) (s ×ˢ t) = s / t
theorem finset.add_image_prod {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} :
finset.image (λ (x : α × α), x.fst - x.snd) (s ×ˢ t) = s - t
theorem finset.mem_div {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} {a : α} :
a s / t ∃ (b c : α), b s c t b / c = a
theorem finset.mem_sub {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} {a : α} :
a s - t ∃ (b c : α), b s c t b - c = a
@[simp, norm_cast]
theorem finset.coe_sub {α : Type u_2} [decidable_eq α] [has_sub α] (s t : finset α) :
(s - t) = s - t
@[simp, norm_cast]
theorem finset.coe_div {α : Type u_2} [decidable_eq α] [has_div α] (s t : finset α) :
(s / t) = s / t
theorem finset.div_mem_div {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} {a b : α} :
a sb ta / b s / t
theorem finset.sub_mem_sub {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} {a b : α} :
a sb ta - b s - t
theorem finset.sub_card_le {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} :
(s - t).card s.card * t.card
theorem finset.div_card_le {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} :
(s / t).card s.card * t.card
@[simp]
theorem finset.empty_sub {α : Type u_2} [decidable_eq α] [has_sub α] (s : finset α) :
@[simp]
theorem finset.empty_div {α : Type u_2} [decidable_eq α] [has_div α] (s : finset α) :
@[simp]
theorem finset.div_empty {α : Type u_2} [decidable_eq α] [has_div α] (s : finset α) :
@[simp]
theorem finset.sub_empty {α : Type u_2} [decidable_eq α] [has_sub α] (s : finset α) :
@[simp]
theorem finset.div_eq_empty {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} :
s / t = s = t =
@[simp]
theorem finset.sub_eq_empty {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} :
s - t = s = t =
@[simp]
theorem finset.sub_nonempty {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} :
@[simp]
theorem finset.div_nonempty {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} :
theorem finset.nonempty.div {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} :
s.nonemptyt.nonempty(s / t).nonempty
theorem finset.nonempty.sub {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} :
s.nonemptyt.nonempty(s - t).nonempty
theorem finset.nonempty.of_sub_left {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} :
(s - t).nonempty → s.nonempty
theorem finset.nonempty.of_div_left {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} :
(s / t).nonempty → s.nonempty
theorem finset.nonempty.of_div_right {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} :
(s / t).nonempty → t.nonempty
theorem finset.nonempty.of_sub_right {α : Type u_2} [decidable_eq α] [has_sub α] {s t : finset α} :
(s - t).nonempty → t.nonempty
@[simp]
theorem finset.sub_singleton {α : Type u_2} [decidable_eq α] [has_sub α] {s : finset α} (a : α) :
s - {a} = finset.image (λ (_x : α), _x - a) s
@[simp]
theorem finset.div_singleton {α : Type u_2} [decidable_eq α] [has_div α] {s : finset α} (a : α) :
s / {a} = finset.image (λ (_x : α), _x / a) s
@[simp]
theorem finset.singleton_sub {α : Type u_2} [decidable_eq α] [has_sub α] {s : finset α} (a : α) :
@[simp]
theorem finset.singleton_div {α : Type u_2} [decidable_eq α] [has_div α] {s : finset α} (a : α) :
@[simp]
theorem finset.singleton_sub_singleton {α : Type u_2} [decidable_eq α] [has_sub α] (a b : α) :
{a} - {b} = {a - b}
@[simp]
theorem finset.singleton_div_singleton {α : Type u_2} [decidable_eq α] [has_div α] (a b : α) :
{a} / {b} = {a / b}
theorem finset.div_subset_div {α : Type u_2} [decidable_eq α] [has_div α] {s₁ s₂ t₁ t₂ : finset α} :
s₁ s₂t₁ t₂s₁ / t₁ s₂ / t₂
theorem finset.sub_subset_sub {α : Type u_2} [decidable_eq α] [has_sub α] {s₁ s₂ t₁ t₂ : finset α} :
s₁ s₂t₁ t₂s₁ - t₁ s₂ - t₂
theorem finset.sub_subset_sub_left {α : Type u_2} [decidable_eq α] [has_sub α] {s t₁ t₂ : finset α} :
t₁ t₂s - t₁ s - t₂
theorem finset.div_subset_div_left {α : Type u_2} [decidable_eq α] [has_div α] {s t₁ t₂ : finset α} :
t₁ t₂s / t₁ s / t₂
theorem finset.div_subset_div_right {α : Type u_2} [decidable_eq α] [has_div α] {s₁ s₂ t : finset α} :
s₁ s₂s₁ / t s₂ / t
theorem finset.sub_subset_sub_right {α : Type u_2} [decidable_eq α] [has_sub α] {s₁ s₂ t : finset α} :
s₁ s₂s₁ - t s₂ - t
theorem finset.div_subset_iff {α : Type u_2} [decidable_eq α] [has_div α] {s t u : finset α} :
s / t u ∀ (x : α), x s∀ (y : α), y tx / y u
theorem finset.sub_subset_iff {α : Type u_2} [decidable_eq α] [has_sub α] {s t u : finset α} :
s - t u ∀ (x : α), x s∀ (y : α), y tx - y u
theorem finset.union_sub {α : Type u_2} [decidable_eq α] [has_sub α] {s₁ s₂ t : finset α} :
s₁ s₂ - t = s₁ - t (s₂ - t)
theorem finset.union_div {α : Type u_2} [decidable_eq α] [has_div α] {s₁ s₂ t : finset α} :
(s₁ s₂) / t = s₁ / t s₂ / t
theorem finset.sub_union {α : Type u_2} [decidable_eq α] [has_sub α] {s t₁ t₂ : finset α} :
s - (t₁ t₂) = s - t₁ (s - t₂)
theorem finset.div_union {α : Type u_2} [decidable_eq α] [has_div α] {s t₁ t₂ : finset α} :
s / (t₁ t₂) = s / t₁ s / t₂
theorem finset.inter_sub_subset {α : Type u_2} [decidable_eq α] [has_sub α] {s₁ s₂ t : finset α} :
s₁ s₂ - t (s₁ - t) (s₂ - t)
theorem finset.inter_div_subset {α : Type u_2} [decidable_eq α] [has_div α] {s₁ s₂ t : finset α} :
s₁ s₂ / t s₁ / t (s₂ / t)
theorem finset.div_inter_subset {α : Type u_2} [decidable_eq α] [has_div α] {s t₁ t₂ : finset α} :
s / (t₁ t₂) s / t₁ (s / t₂)
theorem finset.sub_inter_subset {α : Type u_2} [decidable_eq α] [has_sub α] {s t₁ t₂ : finset α} :
s - t₁ t₂ (s - t₁) (s - t₂)
theorem finset.subset_sub {α : Type u_2} [decidable_eq α] [has_sub α] {u : finset α} {s t : set α} :
u s - t(∃ (s' t' : finset α), 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} [decidable_eq α] [has_div α] {u : finset α} {s t : set α} :
u s / t(∃ (s' t' : finset α), 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 #

@[protected]
def finset.has_nsmul {α : Type u_2} [decidable_eq α] [has_zero α] [has_add α] :

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

Equations
@[protected]
def finset.has_npow {α : Type u_2} [decidable_eq α] [has_one α] [has_mul α] :

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

Equations
@[protected]
def finset.has_zsmul {α : Type u_2} [decidable_eq α] [has_zero α] [has_add α] [has_neg α] :

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

Equations
@[protected]
def finset.has_zpow {α : Type u_2} [decidable_eq α] [has_one α] [has_mul α] [has_inv α] :

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

Equations
@[protected]
def finset.semigroup {α : Type u_2} [decidable_eq α] [semigroup α] :

finset α is a semigroup under pointwise operations if α is.

Equations
@[protected]
def finset.add_semigroup {α : Type u_2} [decidable_eq α] [add_semigroup α] :

finset α is an add_semigroup under pointwise operations if α is.

Equations
@[protected]

finset α is an add_comm_semigroup under pointwise operations if α is.

Equations
@[protected]

finset α is a comm_semigroup under pointwise operations if α is.

Equations
@[protected]

finset α is an add_zero_class under pointwise operations if α is.

Equations
@[protected]
def finset.mul_one_class {α : Type u_2} [decidable_eq α] [mul_one_class α] :

finset α is a mul_one_class under pointwise operations if α is.

Equations
theorem finset.subset_mul_left {α : Type u_2} [decidable_eq α] [mul_one_class α] (s : finset α) {t : finset α} (ht : 1 t) :
s s * t
theorem finset.subset_add_left {α : Type u_2} [decidable_eq α] [add_zero_class α] (s : finset α) {t : finset α} (ht : 0 t) :
s s + t
theorem finset.subset_mul_right {α : Type u_2} [decidable_eq α] [mul_one_class α] {s : finset α} (t : finset α) (hs : 1 s) :
t s * t
theorem finset.subset_add_right {α : Type u_2} [decidable_eq α] [add_zero_class α] {s : finset α} (t : finset α) (hs : 0 s) :
t s + t
def finset.singleton_monoid_hom {α : Type u_2} [decidable_eq α] [mul_one_class α] :
α →* finset α

The singleton operation as a monoid_hom.

Equations
@[simp]
def finset.coe_monoid_hom {α : Type u_2} [decidable_eq α] [mul_one_class α] :

The coercion from finset to set as a monoid_hom.

Equations
def finset.coe_add_monoid_hom {α : Type u_2} [decidable_eq α] [add_zero_class α] :

The coercion from finset to set as an add_monoid_hom.

Equations
@[simp]
@[simp, norm_cast]
theorem finset.coe_nsmul {α : Type u_2} [decidable_eq α] [add_monoid α] (s : finset α) (n : ) :
(n s) = n s
@[simp, norm_cast]
theorem finset.coe_pow {α : Type u_2} [decidable_eq α] [monoid α] (s : finset α) (n : ) :
(s ^ n) = s ^ n
@[protected]
def finset.monoid {α : Type u_2} [decidable_eq α] [monoid α] :

finset α is a monoid under pointwise operations if α is.

Equations
@[protected]
def finset.add_monoid {α : Type u_2} [decidable_eq α] [add_monoid α] :

finset α is an add_monoid under pointwise operations if α is.

Equations
theorem finset.nsmul_mem_nsmul {α : Type u_2} [decidable_eq α] [add_monoid α] {s : finset α} {a : α} (ha : a s) (n : ) :
n a n s
theorem finset.pow_mem_pow {α : Type u_2} [decidable_eq α] [monoid α] {s : finset α} {a : α} (ha : a s) (n : ) :
a ^ n s ^ n
theorem finset.nsmul_subset_nsmul {α : Type u_2} [decidable_eq α] [add_monoid α] {s t : finset α} (hst : s t) (n : ) :
n s n t
theorem finset.pow_subset_pow {α : Type u_2} [decidable_eq α] [monoid α] {s t : finset α} (hst : s t) (n : ) :
s ^ n t ^ n
theorem finset.pow_subset_pow_of_one_mem {α : Type u_2} [decidable_eq α] [monoid α] {s : finset α} {m n : } (hs : 1 s) :
m ns ^ m s ^ n
theorem finset.nsmul_subset_nsmul_of_zero_mem {α : Type u_2} [decidable_eq α] [add_monoid α] {s : finset α} {m n : } (hs : 0 s) :
m nm s n s
@[simp, norm_cast]
theorem finset.coe_list_prod {α : Type u_2} [decidable_eq α] [monoid α] (s : list (finset α)) :
@[simp, norm_cast]
theorem finset.coe_list_sum {α : Type u_2} [decidable_eq α] [add_monoid α] (s : list (finset α)) :
theorem finset.mem_sum_list_of_fn {α : Type u_2} [decidable_eq α] [add_monoid α] {n : } {a : α} {s : fin nfinset α} :
a (list.of_fn s).sum ∃ (f : Π (i : fin n), (s i)), (list.of_fn (λ (i : fin n), (f i))).sum = a
theorem finset.mem_prod_list_of_fn {α : Type u_2} [decidable_eq α] [monoid α] {n : } {a : α} {s : fin nfinset α} :
a (list.of_fn s).prod ∃ (f : Π (i : fin n), (s i)), (list.of_fn (λ (i : fin n), (f i))).prod = a
theorem finset.mem_nsmul {α : Type u_2} [decidable_eq α] [add_monoid α] {s : finset α} {a : α} {n : } :
a n s ∃ (f : fin ns), (list.of_fn (λ (i : fin n), (f i))).sum = a
theorem finset.mem_pow {α : Type u_2} [decidable_eq α] [monoid α] {s : finset α} {a : α} {n : } :
a s ^ n ∃ (f : fin ns), (list.of_fn (λ (i : fin n), (f i))).prod = a
@[simp]
theorem finset.empty_pow {α : Type u_2} [decidable_eq α] [monoid α] {n : } (hn : n 0) :
@[simp]
theorem finset.empty_nsmul {α : Type u_2} [decidable_eq α] [add_monoid α] {n : } (hn : n 0) :
theorem finset.mul_univ_of_one_mem {α : Type u_2} [decidable_eq α] [monoid α] {s : finset α} [fintype α] (hs : 1 s) :
theorem finset.add_univ_of_zero_mem {α : Type u_2} [decidable_eq α] [add_monoid α] {s : finset α} [fintype α] (hs : 0 s) :
theorem finset.univ_mul_of_one_mem {α : Type u_2} [decidable_eq α] [monoid α] {t : finset α} [fintype α] (ht : 1 t) :
theorem finset.univ_add_of_zero_mem {α : Type u_2} [decidable_eq α] [add_monoid α] {t : finset α} [fintype α] (ht : 0 t) :
@[simp]
@[simp]
@[simp]
theorem finset.nsmul_univ {α : Type u_2} [decidable_eq α] [add_monoid α] {n : } [fintype α] (hn : n 0) :
@[simp]
theorem finset.univ_pow {α : Type u_2} [decidable_eq α] [monoid α] {n : } [fintype α] (hn : n 0) :
@[protected]
theorem is_add_unit.finset {α : Type u_2} [decidable_eq α] [add_monoid α] {a : α} :
@[protected]
theorem is_unit.finset {α : Type u_2} [decidable_eq α] [monoid α] {a : α} :
is_unit ais_unit {a}
@[protected]
def finset.comm_monoid {α : Type u_2} [decidable_eq α] [comm_monoid α] :

finset α is a comm_monoid under pointwise operations if α is.

Equations
@[protected]

finset α is an add_comm_monoid under pointwise operations if α is.

Equations
@[simp, norm_cast]
theorem finset.coe_prod {α : Type u_2} [decidable_eq α] [comm_monoid α] {ι : Type u_1} (s : finset ι) (f : ι → finset α) :
(s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), (f i))
@[simp, norm_cast]
theorem finset.coe_sum {α : Type u_2} [decidable_eq α] [add_comm_monoid α] {ι : Type u_1} (s : finset ι) (f : ι → finset α) :
(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), (f i))
@[simp]
theorem finset.coe_zsmul {α : Type u_2} [decidable_eq α] [subtraction_monoid α] (s : finset α) (n : ) :
(n s) = n s
@[simp]
theorem finset.coe_zpow {α : Type u_2} [decidable_eq α] [division_monoid α] (s : finset α) (n : ) :
(s ^ n) = s ^ n
@[protected]
theorem finset.mul_eq_one_iff {α : Type u_2} [decidable_eq α] [division_monoid α] {s t : finset α} :
s * t = 1 ∃ (a b : α), s = {a} t = {b} a * b = 1
@[protected]
theorem finset.add_eq_zero_iff {α : Type u_2} [decidable_eq α] [subtraction_monoid α] {s t : finset α} :
s + t = 0 ∃ (a b : α), s = {a} t = {b} a + b = 0
@[protected]

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

Equations
@[protected]

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

Equations
@[simp]
theorem finset.is_add_unit_iff {α : Type u_2} [decidable_eq α] [subtraction_monoid α] {s : finset α} :
is_add_unit s ∃ (a : α), s = {a} is_add_unit a
@[simp]
theorem finset.is_unit_iff {α : Type u_2} [decidable_eq α] [division_monoid α] {s : finset α} :
is_unit s ∃ (a : α), s = {a} is_unit a
@[simp]
theorem finset.is_add_unit_coe {α : Type u_2} [decidable_eq α] [subtraction_monoid α] {s : finset α} :
@[simp]
theorem finset.is_unit_coe {α : Type u_2} [decidable_eq α] [division_monoid α] {s : finset α} :
@[protected]

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

Equations
@[protected]

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

Equations
@[protected]

finset α has distributive negation if α has.

Equations

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} [decidable_eq α] [distrib α] (s t u : finset α) :
s * (t + u) s * t + s * u
theorem finset.add_mul_subset {α : Type u_2} [decidable_eq α] [distrib α] (s t u : finset α) :
(s + t) * u s * u + t * u

Note that finset is not a mul_zero_class because 0 * ∅ ≠ 0.

theorem finset.mul_zero_subset {α : Type u_2} [decidable_eq α] [mul_zero_class α] (s : finset α) :
s * 0 0
theorem finset.zero_mul_subset {α : Type u_2} [decidable_eq α] [mul_zero_class α] (s : finset α) :
0 * s 0
theorem finset.nonempty.mul_zero {α : Type u_2} [decidable_eq α] [mul_zero_class α] {s : finset α} (hs : s.nonempty) :
s * 0 = 0
theorem finset.nonempty.zero_mul {α : Type u_2} [decidable_eq α] [mul_zero_class α] {s : finset α} (hs : s.nonempty) :
0 * s = 0

Note that finset is not a group because s / s ≠ 1 in general.

@[simp]
theorem finset.one_mem_div_iff {α : Type u_2} [decidable_eq α] [group α] {s t : finset α} :
1 s / t ¬disjoint s t
@[simp]
theorem finset.zero_mem_sub_iff {α : Type u_2} [decidable_eq α] [add_group α] {s t : finset α} :
0 s - t ¬disjoint s t
theorem finset.not_one_mem_div_iff {α : Type u_2} [decidable_eq α] [group α] {s t : finset α} :
1 s / t disjoint s t
theorem finset.not_zero_mem_sub_iff {α : Type u_2} [decidable_eq α] [add_group α] {s t : finset α} :
0 s - t disjoint s t
theorem finset.nonempty.zero_mem_sub {α : Type u_2} [decidable_eq α] [add_group α] {s : finset α} (h : s.nonempty) :
0 s - s
theorem finset.nonempty.one_mem_div {α : Type u_2} [decidable_eq α] [group α] {s : finset α} (h : s.nonempty) :
1 s / s
theorem finset.is_add_unit_singleton {α : Type u_2} [decidable_eq α] [add_group α] (a : α) :
theorem finset.is_unit_singleton {α : Type u_2} [decidable_eq α] [group α] (a : α) :
@[simp]
theorem finset.is_unit_iff_singleton {α : Type u_2} [decidable_eq α] [group α] {s : finset α} :
is_unit s ∃ (a : α), s = {a}
@[simp]
theorem finset.image_mul_left {α : Type u_2} [decidable_eq α] [group α] {t : finset α} {a : α} :
finset.image (λ (b : α), a * b) t = t.preimage (λ (b : α), a⁻¹ * b) _
@[simp]
theorem finset.image_add_left {α : Type u_2} [decidable_eq α] [add_group α] {t : finset α} {a : α} :
finset.image (λ (b : α), a + b) t = t.preimage (λ (b : α), -a + b) _
@[simp]
theorem finset.image_mul_right {α : Type u_2} [decidable_eq α] [group α] {t : finset α} {b : α} :
finset.image (λ (_x : α), _x * b) t = t.preimage (λ (_x : α), _x * b⁻¹) _
@[simp]
theorem finset.image_add_right {α : Type u_2} [decidable_eq α] [add_group α] {t : finset α} {b : α} :
finset.image (λ (_x : α), _x + b) t = t.preimage (λ (_x : α), _x + -b) _
theorem finset.image_add_left' {α : Type u_2} [decidable_eq α] [add_group α] {t : finset α} {a : α} :
finset.image (λ (b : α), -a + b) t = t.preimage (λ (b : α), a + b) _
theorem finset.image_mul_left' {α : Type u_2} [decidable_eq α] [group α] {t : finset α} {a : α} :
finset.image (λ (b : α), a⁻¹ * b) t = t.preimage (λ (b : α), a * b) _
theorem finset.image_add_right' {α : Type u_2} [decidable_eq α] [add_group α] {t : finset α} {b : α} :
finset.image (λ (_x : α), _x + -b) t = t.preimage (λ (_x : α), _x + b) _
theorem finset.image_mul_right' {α : Type u_2} [decidable_eq α] [group α] {t : finset α} {b : α} :
finset.image (λ (_x : α), _x * b⁻¹) t = t.preimage (λ (_x : α), _x * b) _
theorem finset.image_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [decidable_eq α] [decidable_eq β] [group α] [division_monoid β] [monoid_hom_class F α β] (m : F) {s t : finset α} :
theorem finset.div_zero_subset {α : Type u_2} [decidable_eq α] [group_with_zero α] (s : finset α) :
s / 0 0
theorem finset.zero_div_subset {α : Type u_2} [decidable_eq α] [group_with_zero α] (s : finset α) :
0 / s 0
theorem finset.nonempty.div_zero {α : Type u_2} [decidable_eq α] [group_with_zero α] {s : finset α} (hs : s.nonempty) :
s / 0 = 0
theorem finset.nonempty.zero_div {α : Type u_2} [decidable_eq α] [group_with_zero α] {s : finset α} (hs : s.nonempty) :
0 / s = 0
@[simp]
theorem finset.preimage_mul_left_singleton {α : Type u_2} [group α] {a b : α} :
{b}.preimage (has_mul.mul a) _ = {a⁻¹ * b}
@[simp]
theorem finset.preimage_add_left_singleton {α : Type u_2} [add_group α] {a b : α} :
{b}.preimage (has_add.add a) _ = {-a + b}
@[simp]
theorem finset.preimage_mul_right_singleton {α : Type u_2} [group α] {a b : α} :
{b}.preimage (λ (_x : α), _x * a) _ = {b * a⁻¹}
@[simp]
theorem finset.preimage_add_right_singleton {α : Type u_2} [add_group α] {a b : α} :
{b}.preimage (λ (_x : α), _x + a) _ = {b + -a}
@[simp]
theorem finset.preimage_mul_left_one {α : Type u_2} [group α] {a : α} :
@[simp]
theorem finset.preimage_add_left_zero {α : Type u_2} [add_group α] {a : α} :
0.preimage (has_add.add a) _ = {-a}
@[simp]
theorem finset.preimage_add_right_zero {α : Type u_2} [add_group α] {b : α} :
0.preimage (λ (_x : α), _x + b) _ = {-b}
@[simp]
theorem finset.preimage_mul_right_one {α : Type u_2} [group α] {b : α} :
1.preimage (λ (_x : α), _x * b) _ = {b⁻¹}
theorem finset.preimage_add_left_zero' {α : Type u_2} [add_group α] {a : α} :
0.preimage (has_add.add (-a)) _ = {a}
theorem finset.preimage_mul_left_one' {α : Type u_2} [group α] {a : α} :
theorem finset.preimage_mul_right_one' {α : Type u_2} [group α] {b : α} :
1.preimage (λ (_x : α), _x * b⁻¹) _ = {b}
theorem finset.preimage_add_right_zero' {α : Type u_2} [add_group α] {b : α} :
0.preimage (λ (_x : α), _x + -b) _ = {b}

Scalar addition/multiplication of finsets #

@[protected]
def finset.has_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] :

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

Equations
@[protected]
def finset.has_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] :

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

Equations
theorem finset.smul_def {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} :
s t = finset.image (λ (p : α × β), p.fst p.snd) (s ×ˢ t)
theorem finset.vadd_def {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} :
s +ᵥ t = finset.image (λ (p : α × β), p.fst +ᵥ p.snd) (s ×ˢ t)
theorem finset.image_smul_product {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} :
finset.image (λ (x : α × β), x.fst x.snd) (s ×ˢ t) = s t
theorem finset.image_vadd_product {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} :
finset.image (λ (x : α × β), x.fst +ᵥ x.snd) (s ×ˢ t) = s +ᵥ t
theorem finset.mem_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} {x : β} :
x s t ∃ (y : α) (z : β), y s z t y z = x
theorem finset.mem_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} {x : β} :
x s +ᵥ t ∃ (y : α) (z : β), y s z t y +ᵥ z = x
@[simp, norm_cast]
theorem finset.coe_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] (s : finset α) (t : finset β) :
(s +ᵥ t) = s +ᵥ t
@[simp, norm_cast]
theorem finset.coe_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] (s : finset α) (t : finset β) :
(s t) = s t
theorem finset.vadd_mem_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} {a : α} {b : β} :
a sb ta +ᵥ b s +ᵥ t
theorem finset.smul_mem_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} {a : α} {b : β} :
a sb ta b s t
theorem finset.vadd_card_le {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} :
(s +ᵥ t).card s.card t.card
theorem finset.smul_card_le {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} :
(s t).card s.card t.card
@[simp]
theorem finset.empty_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] (t : finset β) :
@[simp]
theorem finset.empty_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] (t : finset β) :
@[simp]
theorem finset.vadd_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] (s : finset α) :
@[simp]
theorem finset.smul_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] (s : finset α) :
@[simp]
theorem finset.vadd_eq_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} :
s +ᵥ t = s = t =
@[simp]
theorem finset.smul_eq_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} :
s t = s = t =
@[simp]
theorem finset.smul_nonempty_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} :
@[simp]
theorem finset.vadd_nonempty_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} :
theorem finset.nonempty.smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} :
s.nonemptyt.nonempty(s t).nonempty
theorem finset.nonempty.vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} :
s.nonemptyt.nonempty(s +ᵥ t).nonempty
theorem finset.nonempty.of_vadd_left {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} :
(s +ᵥ t).nonempty → s.nonempty
theorem finset.nonempty.of_smul_left {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} :
(s t).nonempty → s.nonempty
theorem finset.nonempty.of_vadd_right {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t : finset β} :
(s +ᵥ t).nonempty → t.nonempty
theorem finset.nonempty.of_smul_right {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t : finset β} :
(s t).nonempty → t.nonempty
theorem finset.vadd_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} (b : β) :
s +ᵥ {b} = finset.image (λ (_x : α), _x +ᵥ b) s
theorem finset.smul_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} (b : β) :
s {b} = finset.image (λ (_x : α), _x b) s
theorem finset.singleton_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {t : finset β} (a : α) :
theorem finset.singleton_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {t : finset β} (a : α) :
@[simp]
theorem finset.singleton_vadd_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] (a : α) (b : β) :
{a} +ᵥ {b} = {a +ᵥ b}
@[simp]
theorem finset.singleton_smul_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] (a : α) (b : β) :
{a} {b} = {a b}
theorem finset.smul_subset_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s₁ s₂ : finset α} {t₁ t₂ : finset β} :
s₁ s₂t₁ t₂s₁ t₁ s₂ t₂
theorem finset.vadd_subset_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s₁ s₂ : finset α} {t₁ t₂ : finset β} :
s₁ s₂t₁ t₂s₁ +ᵥ t₁ s₂ +ᵥ t₂
theorem finset.vadd_subset_vadd_left {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t₁ t₂ : finset β} :
t₁ t₂s +ᵥ t₁ s +ᵥ t₂
theorem finset.smul_subset_smul_left {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t₁ t₂ : finset β} :
t₁ t₂s t₁ s t₂
theorem finset.vadd_subset_vadd_right {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s₁ s₂ : finset α} {t : finset β} :
s₁ s₂s₁ +ᵥ t s₂ +ᵥ t
theorem finset.smul_subset_smul_right {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s₁ s₂ : finset α} {t : finset β} :
s₁ s₂s₁ t s₂ t
theorem finset.smul_subset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t u : finset β} :
s t u ∀ (a : α), a s∀ (b : β), b ta b u
theorem finset.vadd_subset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t u : finset β} :
s +ᵥ t u ∀ (a : α), a s∀ (b : β), b ta +ᵥ b u
theorem finset.union_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s₁ s₂ : finset α} {t : finset β} [decidable_eq α] :
(s₁ s₂) t = s₁ t s₂ t
theorem finset.union_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s₁ s₂ : finset α} {t : finset β} [decidable_eq α] :
s₁ s₂ +ᵥ t = s₁ +ᵥ t (s₂ +ᵥ t)
theorem finset.vadd_union {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t₁ t₂ : finset β} :
s +ᵥ (t₁ t₂) = s +ᵥ t₁ (s +ᵥ t₂)
theorem finset.smul_union {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t₁ t₂ : finset β} :
s (t₁ t₂) = s t₁ s t₂
theorem finset.inter_vadd_subset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s₁ s₂ : finset α} {t : finset β} [decidable_eq α] :
s₁ s₂ +ᵥ t (s₁ +ᵥ t) (s₂ +ᵥ t)
theorem finset.inter_smul_subset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s₁ s₂ : finset α} {t : finset β} [decidable_eq α] :
(s₁ s₂) t s₁ t s₂ t
theorem finset.smul_inter_subset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset α} {t₁ t₂ : finset β} :
s (t₁ t₂) s t₁ s t₂
theorem finset.vadd_inter_subset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset α} {t₁ t₂ : finset β} :
s +ᵥ t₁ t₂ (s +ᵥ t₁) (s +ᵥ t₂)
theorem finset.subset_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {u : finset β} {s : set α} {t : set β} :
u s +ᵥ t(∃ (s' : finset α) (t' : finset β), 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} [decidable_eq β] [has_smul α β] {u : finset β} {s : set α} {t : set β} :
u s t(∃ (s' : finset α) (t' : finset β), 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 #

@[protected]
def finset.has_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] :

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

Equations
theorem finset.vsub_def {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} :
@[simp]
theorem finset.image_vsub_product {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} :
theorem finset.mem_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} {a : α} :
a s -ᵥ t ∃ (b c : β), b s c t b -ᵥ c = a
@[simp, norm_cast]
theorem finset.coe_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] (s t : finset β) :
(s -ᵥ t) = s -ᵥ t
theorem finset.vsub_mem_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} {b c : β} :
b sc tb -ᵥ c s -ᵥ t
theorem finset.vsub_card_le {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} :
(s -ᵥ t).card s.card * t.card
@[simp]
theorem finset.empty_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] (t : finset β) :
@[simp]
theorem finset.vsub_empty {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] (s : finset β) :
@[simp]
theorem finset.vsub_eq_empty {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} :
s -ᵥ t = s = t =
@[simp]
theorem finset.vsub_nonempty {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} :
theorem finset.nonempty.vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} :
s.nonemptyt.nonempty(s -ᵥ t).nonempty
theorem finset.nonempty.of_vsub_left {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} :
(s -ᵥ t).nonempty → s.nonempty
theorem finset.nonempty.of_vsub_right {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} :
(s -ᵥ t).nonempty → t.nonempty
@[simp]
theorem finset.vsub_singleton {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s : finset β} (b : β) :
s -ᵥ {b} = finset.image (λ (_x : β), _x -ᵥ b) s
theorem finset.singleton_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {t : finset β} (a : β) :
@[simp]
theorem finset.singleton_vsub_singleton {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] (a b : β) :
{a} -ᵥ {b} = {a -ᵥ b}
theorem finset.vsub_subset_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s₁ s₂ t₁ t₂ : finset β} :
s₁ s₂t₁ t₂s₁ -ᵥ t₁ s₂ -ᵥ t₂
theorem finset.vsub_subset_vsub_left {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t₁ t₂ : finset β} :
t₁ t₂s -ᵥ t₁ s -ᵥ t₂
theorem finset.vsub_subset_vsub_right {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s₁ s₂ t : finset β} :
s₁ s₂s₁ -ᵥ t s₂ -ᵥ t
theorem finset.vsub_subset_iff {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t : finset β} {u : finset α} :
s -ᵥ t u ∀ (x : β), x s∀ (y : β), y tx -ᵥ y u
theorem finset.union_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s₁ s₂ t : finset β} [decidable_eq β] :
s₁ s₂ -ᵥ t = s₁ -ᵥ t (s₂ -ᵥ t)
theorem finset.vsub_union {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t₁ t₂ : finset β} [decidable_eq β] :
s -ᵥ (t₁ t₂) = s -ᵥ t₁ (s -ᵥ t₂)
theorem finset.inter_vsub_subset {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s₁ s₂ t : finset β} [decidable_eq β] :
s₁ s₂ -ᵥ t (s₁ -ᵥ t) (s₂ -ᵥ t)
theorem finset.vsub_inter_subset {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {s t₁ t₂ : finset β} [decidable_eq β] :
s -ᵥ t₁ t₂ (s -ᵥ t₁) (s -ᵥ t₂)
theorem finset.subset_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [has_vsub α β] {u : finset α} {s t : set β} :
u s -ᵥ t(∃ (s' t' : finset β), 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 #

@[protected]
def finset.has_vadd_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] :

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

Equations
@[protected]
def finset.has_smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] :

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

Equations
theorem finset.smul_finset_def {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset β} {a : α} :
theorem finset.vadd_finset_def {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset β} {a : α} :
theorem finset.image_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset β} {a : α} :
finset.image (λ (x : β), a +ᵥ x) s = a +ᵥ s
theorem finset.image_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset β} {a : α} :
finset.image (λ (x : β), a x) s = a s
theorem finset.mem_smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset β} {a : α} {x : β} :
x a s ∃ (y : β), y s a y = x
theorem finset.mem_vadd_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset β} {a : α} {x : β} :
x a +ᵥ s ∃ (y : β), y s a +ᵥ y = x
@[simp, norm_cast]
theorem finset.coe_smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] (a : α) (s : finset β) :
(a s) = a s
@[simp, norm_cast]
theorem finset.coe_vadd_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] (a : α) (s : finset β) :
(a +ᵥ s) = a +ᵥ s
theorem finset.vadd_finset_mem_vadd_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset β} {a : α} {b : β} :
b sa +ᵥ b a +ᵥ s
theorem finset.smul_finset_mem_smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset β} {a : α} {b : β} :
b sa b a s
theorem finset.vadd_finset_card_le {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset β} {a : α} :
(a +ᵥ s).card s.card
theorem finset.smul_finset_card_le {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset β} {a : α} :
(a s).card s.card
@[simp]
theorem finset.vadd_finset_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] (a : α) :
@[simp]
theorem finset.smul_finset_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] (a : α) :
@[simp]
theorem finset.vadd_finset_eq_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset β} {a : α} :
a +ᵥ s = s =
@[simp]
theorem finset.smul_finset_eq_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset β} {a : α} :
a s = s =
@[simp]
theorem finset.vadd_finset_nonempty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset β} {a : α} :
@[simp]
theorem finset.smul_finset_nonempty {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset β} {a : α} :
theorem finset.nonempty.vadd_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s : finset β} {a : α} (hs : s.nonempty) :
theorem finset.nonempty.smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s : finset β} {a : α} (hs : s.nonempty) :
theorem finset.vadd_finset_subset_vadd_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s t : finset β} {a : α} :
s ta +ᵥ s a +ᵥ t
theorem finset.smul_finset_subset_smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s t : finset β} {a : α} :
s ta s a t
@[simp]
theorem finset.smul_finset_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {a : α} (b : β) :
a {b} = {a b}
@[simp]
theorem finset.vadd_finset_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {a : α} (b : β) :
a +ᵥ {b} = {a +ᵥ b}
theorem finset.vadd_finset_union {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s₁ s₂ : finset β} {a : α} :
a +ᵥ (s₁ s₂) = a +ᵥ s₁ (a +ᵥ s₂)
theorem finset.smul_finset_union {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s₁ s₂ : finset β} {a : α} :
a (s₁ s₂) = a s₁ a s₂
theorem finset.smul_finset_inter_subset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] {s₁ s₂ : finset β} {a : α} :
a (s₁ s₂) a s₁ a s₂
theorem finset.vadd_finset_inter_subset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_vadd α β] {s₁ s₂ : finset β} {a : α} :
a +ᵥ s₁ s₂ (a +ᵥ s₁) (a +ᵥ s₂)
@[simp]
theorem finset.bUnion_smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] (s : finset α) (t : finset β) :
s.bUnion (λ (_x : α), _x t) = s t
@[protected, instance]
def finset.vadd_comm_class_finset {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_vadd α γ] [has_vadd β γ] [vadd_comm_class α β γ] :
@[protected, instance]
def finset.smul_comm_class_finset {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :
@[protected, instance]
def finset.vadd_comm_class_finset' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_vadd α γ] [has_vadd β γ] [vadd_comm_class α β γ] :
@[protected, instance]
def finset.smul_comm_class_finset' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :
@[protected, instance]
def finset.vadd_comm_class_finset'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_vadd α γ] [has_vadd β γ] [vadd_comm_class α β γ] :
@[protected, instance]
def finset.smul_comm_class_finset'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :
@[protected, instance]
def finset.vadd_comm_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_vadd α γ] [has_vadd β γ] [vadd_comm_class α β γ] :
@[protected, instance]
def finset.smul_comm_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :
@[protected, instance]
def finset.is_scalar_tower {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_smul α β] [has_smul α γ] [has_smul β γ] [is_scalar_tower α β γ] :
@[protected, instance]
def finset.vadd_assoc_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [has_vadd α β] [has_vadd α γ] [has_vadd β γ] [vadd_assoc_class α β γ] :
@[protected, instance]
def finset.is_scalar_tower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [decidable_eq β] [has_smul α β] [has_smul α γ] [has_smul β γ] [is_scalar_tower α β γ] :
@[protected, instance]
def finset.vadd_assoc_class' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [decidable_eq β] [has_vadd α β] [has_vadd α γ] [has_vadd β γ] [vadd_assoc_class α β γ] :
@[protected, instance]
def finset.vadd_assoc_class'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [decidable_eq β] [has_vadd α β] [has_vadd α γ] [has_vadd β γ] [vadd_assoc_class α β γ] :
@[protected, instance]
def finset.is_scalar_tower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [decidable_eq β] [has_smul α β] [has_smul α γ] [has_smul β γ] [is_scalar_tower α β γ] :
@[protected, instance]
def finset.is_central_scalar {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_smul α β] [has_smul αᵐᵒᵖ β] [is_central_scalar α β] :
@[protected]
def finset.mul_action {α : Type u_2} {β : Type u_3} [decidable_eq β] [decidable_eq α] [monoid α] [mul_action α β] :

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

Equations
@[protected]
def finset.add_action {α : Type u_2} {β : Type u_3} [decidable_eq β] [decidable_eq α] [add_monoid α] [add_action α β] :

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

Equations
@[protected]
def finset.add_action_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_monoid α] [add_action α β] :

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

Equations
@[protected]
def finset.mul_action_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [monoid α] [mul_action α β] :

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

Equations
@[protected]
def finset.distrib_mul_action_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [monoid α] [add_monoid β] [distrib_mul_action α β] :

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

Equations
@[protected]
def finset.mul_distrib_mul_action_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [monoid α] [monoid β] [mul_distrib_mul_action α β] :

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

Equations
@[protected, instance]
@[protected, instance]
def finset.no_zero_smul_divisors {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_zero α] [has_zero β] [has_smul α β] [no_zero_smul_divisors α β] :
@[protected, instance]
def finset.no_zero_smul_divisors_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_zero α] [has_zero β] [has_smul α β] [no_zero_smul_divisors α β] :
theorem finset.pairwise_disjoint_smul_iff {α : Type u_2} [left_cancel_semigroup α] [decidable_eq α] {s : set α} {t : finset α} :
s.pairwise_disjoint (λ (_x : α), _x t) set.inj_on (λ (p : α × α), p.fst * p.snd) (s ×ˢ t)
theorem finset.pairwise_disjoint_vadd_iff {α : Type u_2} [add_left_cancel_semigroup α] [decidable_eq α] {s : set α} {t : finset α} :
s.pairwise_disjoint (λ (_x : α), _x +ᵥ t) set.inj_on (λ (p : α × α), p.fst + p.snd) (s ×ˢ t)
@[simp]
theorem finset.card_singleton_add {α : Type u_2} [add_left_cancel_semigroup α] [decidable_eq α] (t : finset α) (a : α) :
({a} + t).card = t.card
@[simp]
theorem finset.card_singleton_mul {α : Type u_2} [left_cancel_semigroup α] [decidable_eq α] (t : finset α) (a : α) :
({a} * t).card = t.card
theorem finset.singleton_mul_inter {α : Type u_2} [left_cancel_semigroup α] [decidable_eq α] (s t : finset α) (a : α) :
{a} * (s t) = {a} * s ({a} * t)
theorem finset.singleton_add_inter {α : Type u_2} [add_left_cancel_semigroup α] [decidable_eq α] (s t : finset α) (a : α) :
{a} + s t = ({a} + s) ({a} + t)
theorem finset.card_le_card_add_left {α : Type u_2} [add_left_cancel_semigroup α] [decidable_eq α] (t : finset α) {s : finset α} (hs : s.nonempty) :
t.card (s + t).card
theorem finset.card_le_card_mul_left {α : Type u_2} [left_cancel_semigroup α] [decidable_eq α] (t : finset α) {s : finset α} (hs : s.nonempty) :
t.card (s * t).card
@[simp]
theorem finset.card_add_singleton {α : Type u_2} [add_right_cancel_semigroup α] [decidable_eq α] (s : finset α) (a : α) :
(s + {a}).card = s.card
@[simp]
theorem finset.card_mul_singleton {α : Type u_2} [right_cancel_semigroup α] [decidable_eq α] (s : finset α) (a : α) :
(s * {a}).card = s.card
theorem finset.inter_add_singleton {α : Type u_2} [add_right_cancel_semigroup α] [decidable_eq α] (s t : finset α) (a : α) :
s t + {a} = (s + {a}) (t + {a})
theorem finset.inter_mul_singleton {α : Type u_2} [right_cancel_semigroup α] [decidable_eq α] (s t : finset α) (a : α) :
s t * {a} = s * {a} (t * {a})
theorem finset.card_le_card_add_right {α : Type u_2} [add_right_cancel_semigroup α] [decidable_eq α] (s : finset α) {t : finset α} (ht : t.nonempty) :
s.card (s + t).card
theorem finset.card_le_card_mul_right {α : Type u_2} [right_cancel_semigroup α] [decidable_eq α] (s : finset α) {t : finset α} (ht : t.nonempty) :
s.card (s * t).card
@[simp]
theorem finset.vadd_mem_vadd_finset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_group α] [add_action α β] {s : finset β} {b : β} (a : α) :
a +ᵥ b a +ᵥ s b s
@[simp]
theorem finset.smul_mem_smul_finset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [group α] [mul_action α β] {s : finset β} {b : β} (a : α) :
a b a s b s
theorem finset.neg_vadd_mem_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_group α] [add_action α β] {s : finset β} {a : α} {b : β} :
-a +ᵥ b s b a +ᵥ s
theorem finset.inv_smul_mem_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [group α] [mul_action α β] {s : finset β} {a : α} {b : β} :
a⁻¹ b s b a s
theorem finset.mem_inv_smul_finset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [group α] [mul_action α β] {s : finset β} {a : α} {b : β} :
b a⁻¹ s a b s
theorem finset.mem_neg_vadd_finset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_group α] [add_action α β] {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} [decidable_eq β] [add_group α] [add_action α β] {s t : finset β} {a : α} :
a +ᵥ s a +ᵥ t s t
@[simp]
theorem finset.smul_finset_subset_smul_finset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [group α] [mul_action α β] {s t : finset β} {a : α} :
a s a t s t
theorem finset.vadd_finset_subset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_group α] [add_action α β] {s t : finset β} {a : α} :
a +ᵥ s t s -a +ᵥ t
theorem finset.smul_finset_subset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [group α] [mul_action α β] {s t : finset β} {a : α} :
a s t s a⁻¹ t
theorem finset.subset_vadd_finset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [add_group α] [add_action α β] {s t : finset β} {a : α} :
s a +ᵥ t -a +ᵥ s t
theorem finset.subset_smul_finset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [group α] [mul_action α β] {s t : finset β} {a : α} :
s a t a⁻¹ s t
@[simp]
theorem finset.smul_mem_smul_finset_iff₀ {α : Type u_2} {β : Type u_3} [decidable_eq β] [group_with_zero α] [mul_action α β] {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} [decidable_eq β] [group_with_zero α] [mul_action α β] {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} [decidable_eq β] [group_with_zero α] [mul_action α β] {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} [decidable_eq β] [group_with_zero α] [mul_action α β] {s t : finset β} {a : α} (ha : a 0) :
a s a t s t
theorem finset.smul_finset_subset_iff₀ {α : Type u_2} {β : Type u_3} [decidable_eq β] [group_with_zero α] [mul_action α β] {s t : finset β} {a : α} (ha : a 0) :
a s t s a⁻¹ t
theorem finset.subset_smul_finset_iff₀ {α : Type u_2} {β : Type u_3} [decidable_eq β] [group_with_zero α] [mul_action α β] {s t : finset β} {a : α} (ha : a 0) :
s a t a⁻¹ s t
theorem finset.smul_univ₀ {α : Type u_2} {β : Type u_3} [decidable_eq β] [group_with_zero α] [mul_action α β] [fintype β] {s : finset α} (hs : ¬s 0) :
theorem finset.smul_finset_univ₀ {α : Type u_2} {β : Type u_3} [decidable_eq β] [group_with_zero α] [mul_action α β] {a : α} [fintype β] (ha : a 0) :

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

theorem finset.smul_zero_subset {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] [decidable_eq β] (s : finset α) :
s 0 0
theorem finset.zero_smul_subset {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] [decidable_eq β] (t : finset β) :
0 t 0
theorem finset.nonempty.smul_zero {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] [decidable_eq β] {s : finset α} (hs : s.nonempty) :
s 0 = 0
theorem finset.nonempty.zero_smul {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] [decidable_eq β] {t : finset β} (ht : t.nonempty) :
0 t = 0
theorem finset.zero_smul_finset {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] [decidable_eq β] {s : finset β} (h : s.nonempty) :
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} [has_zero α] [has_zero β] [smul_with_zero α β] [decidable_eq β] (s : finset β) :
0 s 0
theorem finset.zero_mem_smul_finset {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] [decidable_eq β] {t : finset β} {a : α} (h : 0 t) :
0 a t
theorem finset.zero_mem_smul_iff {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] [decidable_eq β] {s : finset α} {t : finset β} [no_zero_smul_divisors α β] :
0 s t 0 s t.nonempty 0 t s.nonempty
theorem finset.zero_mem_smul_finset_iff {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] [decidable_eq β] {t : finset β} [no_zero_smul_divisors α β] {a : α} (ha : a 0) :
0 a t 0 t
@[simp]
theorem finset.smul_finset_neg {α : Type u_2} {β : Type u_3} [monoid α] [add_group β] [distrib_mul_action α β] [decidable_eq β] (a : α) (t : finset β) :
a -t = -(a t)
@[protected, simp]
theorem finset.smul_neg {α : Type u_2} {β : Type u_3} [monoid α] [add_group β] [distrib_mul_action α β] [decidable_eq β] (s : finset α) (t : finset β) :
s -t = -(s t)
@[simp]
theorem finset.neg_smul_finset {α : Type u_2} {β : Type u_3} [ring α] [add_comm_group β] [module α β] [decidable_eq β] {t : finset β} {a : α} :
-a t = -(a t)
@[protected, simp]
theorem finset.neg_smul {α : Type u_2} {β : Type u_3} [ring α] [add_comm_group β] [module α β] [decidable_eq β] {s : finset α} {t : finset β} [decidable_eq α] :
-s t = -(s t)