# mathlibdocumentation

data.finset.pointwise

# Pointwise operations of finsets #

This file defines pointwise algebraic operations on finsets.

## Main declarations #

For finsets `s` and `t`:

• `0` (`finset.has_zero`): The singleton `{0}`.
• `1` (`finset.has_one`): The singleton `{1}`.
• `-s` (`finset.has_neg`): Negation, finset of all `-x` where `x ∈ s`.
• `s⁻¹` (`finset.has_inv`): Inversion, finset of all `x⁻¹` where `x ∈ s`.
• `s + t` (`finset.has_add`): Addition, finset of all `x + y` where `x ∈ s` and `y ∈ t`.
• `s * t` (`finset.has_mul`): Multiplication, finset of all `x * y` where `x ∈ s` and `y ∈ t`.
• `s - t` (`finset.has_sub`): Subtraction, finset of all `x - y` where `x ∈ s` and `y ∈ t`.
• `s / t` (`finset.has_div`): Division, finset of all `x / y` where `x ∈ s` and `y ∈ t`.
• `s +ᵥ t` (`finset.has_vadd`): Scalar addition, finset of all `x +ᵥ y` where `x ∈ s` and `y ∈ t`.
• `s • t` (`finset.has_smul`): Scalar multiplication, finset of all `x • y` where `x ∈ s` and `y ∈ t`.
• `s -ᵥ t` (`finset.has_vsub`): Scalar subtraction, finset of all `x -ᵥ y` where `x ∈ s` and `y ∈ t`.
• `a • s` (`finset.has_smul_finset`): Scaling, finset of all `a • x` where `x ∈ s`.
• `a +ᵥ s` (`finset.has_vadd_finset`): Translation, finset of all `a +ᵥ x` where `x ∈ s`.

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

## Implementation notes #

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

## Tags #

### `0`/`1` as finsets #

@[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 : α β} :
0 = {f 0}
@[protected, simp]
theorem finset.map_one {α : Type u_2} {β : Type u_3} [has_one α] {f : α β} :
1 = {f 1}
@[simp]
theorem finset.image_zero {α : Type u_2} {β : Type u_3} [has_zero α] [decidable_eq β] {f : α → β} :
0 = {f 0}
@[simp]
theorem finset.image_one {α : Type u_2} {β : Type u_3} [has_one α] [decidable_eq β] {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 α] :
(finset α)

The singleton operation as a `zero_hom`.

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

The singleton operation as a `one_hom`.

Equations
@[simp]
theorem finset.coe_singleton_zero_hom {α : Type u_2} [has_zero α] :
@[simp]
theorem finset.coe_singleton_one_hom {α : Type u_2} [has_one α] :
@[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 α] (s : finset α) :
@[simp, norm_cast]
theorem finset.coe_inv {α : Type u_2} [decidable_eq α] (s : finset α) :
@[simp]
theorem finset.card_inv {α : Type u_2} [decidable_eq α] (s : finset α) :
@[simp]
theorem finset.card_neg {α : Type u_2} [decidable_eq α] (s : finset α) :
(-s).card = s.card
@[simp]
theorem finset.preimage_neg {α : Type u_2} [decidable_eq α] (s : finset α) :
= -s
@[simp]
theorem finset.preimage_inv {α : Type u_2} [decidable_eq α] (s : finset α) :

@[protected]

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 α} :
(s + t).nonempty
@[simp]
theorem finset.mul_nonempty {α : Type u_2} [decidable_eq α] [has_mul α] {s t : finset α} :
(s * t).nonempty
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 : α) :
{a} + s = s
theorem finset.singleton_mul {α : Type u_2} [decidable_eq α] [has_mul α] {s : finset α} (a : α) :
{a} * s = s
@[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 β] [ β] (m : F) {s t : finset α} :
(s + t) = +
theorem finset.image_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [decidable_eq α] [decidable_eq β] [has_mul α] [has_mul β] [ β] (m : F) {s t : finset α} :
(s * t) = *
(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]
@[simp]
theorem finset.coe_singleton_mul_hom {α : Type u_2} [decidable_eq α] [has_mul α] :
@[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 α} :
(s - t).nonempty
@[simp]
theorem finset.div_nonempty {α : Type u_2} [decidable_eq α] [has_div α] {s t : finset α} :
(s / t).nonempty
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 : α) :
{a} - s = s
@[simp]
theorem finset.singleton_div {α : Type u_2} [decidable_eq α] [has_div α] {s : finset α} (a : α) :
{a} / s = s
@[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 α] :
(finset α)

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

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 α]  :

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

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

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

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

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

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

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

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

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

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

The singleton operation as an `add_monoid_hom`.

Equations
def finset.singleton_monoid_hom {α : Type u_2} [decidable_eq α]  :
α →*

The singleton operation as a `monoid_hom`.

Equations
@[simp]
theorem finset.coe_singleton_add_monoid_hom {α : Type u_2} [decidable_eq α]  :
@[simp]
theorem finset.coe_singleton_monoid_hom {α : Type u_2} [decidable_eq α]  :
@[simp]
theorem finset.singleton_add_monoid_hom_apply {α : Type u_2} [decidable_eq α] (a : α) :
@[simp]
theorem finset.singleton_monoid_hom_apply {α : Type u_2} [decidable_eq α] (a : α) :
def finset.coe_monoid_hom {α : Type u_2} [decidable_eq α]  :
→* set α

The coercion from `finset` to `set` as a `monoid_hom`.

Equations
def finset.coe_add_monoid_hom {α : Type u_2} [decidable_eq α]  :
→+ set α

The coercion from `finset` to `set` as an `add_monoid_hom`.

Equations
@[simp]
theorem finset.coe_coe_add_monoid_hom {α : Type u_2} [decidable_eq α]  :
@[simp]
theorem finset.coe_coe_monoid_hom {α : Type u_2} [decidable_eq α]  :
@[simp]
theorem finset.coe_add_monoid_hom_apply {α : Type u_2} [decidable_eq α] (s : finset α) :
@[simp]
theorem finset.coe_monoid_hom_apply {α : Type u_2} [decidable_eq α] (s : finset α) :
@[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
• finset.monoid = finset.monoid._proof_1 finset.monoid._proof_2 finset.monoid._proof_3
@[protected]

`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 α)) :
(s.prod) = s).prod
@[simp, norm_cast]
theorem finset.coe_list_sum {α : Type u_2} [decidable_eq α] [add_monoid α] (s : list (finset α)) :
(s.sum) = s).sum
theorem finset.mem_sum_list_of_fn {α : Type u_2} [decidable_eq α] [add_monoid α] {n : } {a : α} {s : fin n} :
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 n} :
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]
theorem finset.univ_mul_univ {α : Type u_2} [decidable_eq α] [monoid α] [fintype α] :
@[simp]
theorem finset.univ_add_univ {α : Type u_2} [decidable_eq α] [add_monoid α] [fintype α] :
@[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 {a}
@[protected]
def finset.comm_monoid {α : Type u_2} [decidable_eq α] [comm_monoid α] :

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

Equations
• finset.comm_monoid = finset.comm_monoid._proof_1 finset.comm_monoid._proof_2 finset.comm_monoid._proof_3
@[protected]
def finset.add_comm_monoid {α : Type u_2} [decidable_eq α]  :

`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 : ι → ) :
(s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), (f i))
@[simp, norm_cast]
theorem finset.coe_sum {α : Type u_2} [decidable_eq α] {ι : Type u_1} (s : finset ι) (f : ι → ) :
(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), (f i))
@[simp]
theorem finset.coe_zsmul {α : Type u_2} [decidable_eq α] (s : finset α) (n : ) :
(n s) = n s
@[simp]
theorem finset.coe_zpow {α : Type u_2} [decidable_eq α] (s : finset α) (n : ) :
(s ^ n) = s ^ n
@[protected]
theorem finset.mul_eq_one_iff {α : Type u_2} [decidable_eq α] {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 α] {s t : finset α} :
s + t = 0 ∃ (a b : α), s = {a} t = {b} a + b = 0
@[protected]
def finset.division_monoid {α : Type u_2} [decidable_eq α]  :

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

Equations
• finset.division_monoid = finset.division_monoid._proof_1 finset.division_monoid._proof_2 finset.division_monoid._proof_3 finset.division_monoid._proof_4 finset.division_monoid._proof_5 finset.division_monoid._proof_6
@[protected]
def finset.subtraction_monoid {α : Type u_2} [decidable_eq α]  :

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

Equations
• finset.subtraction_monoid = finset.subtraction_monoid._proof_1 finset.subtraction_monoid._proof_2 finset.subtraction_monoid._proof_3 finset.subtraction_monoid._proof_4 finset.subtraction_monoid._proof_5 finset.subtraction_monoid._proof_6
@[simp]
theorem finset.is_add_unit_iff {α : Type u_2} [decidable_eq α] {s : finset α} :
∃ (a : α), s = {a}
@[simp]
theorem finset.is_unit_iff {α : Type u_2} [decidable_eq α] {s : finset α} :
∃ (a : α), s = {a}
@[simp]
theorem finset.is_add_unit_coe {α : Type u_2} [decidable_eq α] {s : finset α} :
@[simp]
theorem finset.is_unit_coe {α : Type u_2} [decidable_eq α] {s : finset α} :
@[protected]
def finset.subtraction_comm_monoid {α : Type u_2} [decidable_eq α]  :

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

Equations
• finset.subtraction_comm_monoid = finset.subtraction_comm_monoid._proof_1 finset.subtraction_comm_monoid._proof_2 finset.subtraction_comm_monoid._proof_3 finset.subtraction_comm_monoid._proof_4 finset.subtraction_comm_monoid._proof_5 finset.subtraction_comm_monoid._proof_6
@[protected]
def finset.division_comm_monoid {α : Type u_2} [decidable_eq α]  :

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

Equations
• finset.division_comm_monoid = finset.division_comm_monoid._proof_1 finset.division_comm_monoid._proof_2 finset.division_comm_monoid._proof_3 finset.division_comm_monoid._proof_4 finset.division_comm_monoid._proof_5 finset.division_comm_monoid._proof_6
@[protected]
def finset.has_distrib_neg {α : Type u_2} [decidable_eq α] [has_mul α]  :

`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 α] (s : finset α) :
s * 0 0
theorem finset.zero_mul_subset {α : Type u_2} [decidable_eq α] (s : finset α) :
0 * s 0
theorem finset.nonempty.mul_zero {α : Type u_2} [decidable_eq α] {s : finset α} (hs : s.nonempty) :
s * 0 = 0
theorem finset.nonempty.zero_mul {α : Type u_2} [decidable_eq α] {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 ¬ t
@[simp]
theorem finset.zero_mem_sub_iff {α : Type u_2} [decidable_eq α] [add_group α] {s t : finset α} :
0 s - t ¬ t
theorem finset.not_one_mem_div_iff {α : Type u_2} [decidable_eq α] [group α] {s t : finset α} :
1 s / t t
theorem finset.not_zero_mem_sub_iff {α : Type u_2} [decidable_eq α] [add_group α] {s t : finset α} :
0 s - t 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 α} :
∃ (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 α] [ β] (m : F) {s t : finset α} :
(s / t) = /
theorem finset.div_zero_subset {α : Type u_2} [decidable_eq α] (s : finset α) :
s / 0 0
theorem finset.zero_div_subset {α : Type u_2} [decidable_eq α] (s : finset α) :
0 / s 0
theorem finset.nonempty.div_zero {α : Type u_2} [decidable_eq α] {s : finset α} (hs : s.nonempty) :
s / 0 = 0
theorem finset.nonempty.zero_div {α : Type u_2} [decidable_eq α] {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 : α} :
@[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 : α} :
@[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 : α} :
theorem finset.preimage_mul_left_one' {α : Type u_2} [group α] {a : α} :
1.preimage _ = {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 β] [ β] :

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 β] [ β] :

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 β] [ β] {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 β] [ β] {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 β] [ β] {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 β] [ β] {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 β] [ β] {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 β] [ β] {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 β] [ β] (s : finset α) (t : finset β) :
(s +ᵥ t) = s +ᵥ t
@[simp, norm_cast]
theorem finset.coe_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] (s : finset α) (t : finset β) :
(s t) = s t
theorem finset.vadd_mem_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {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 β] [ β] {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 β] [ β] {s : finset α} {t : finset β} :
(s +ᵥ t).card s.card t.card
theorem finset.smul_card_le {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset α} {t : finset β} :
(s t).card s.card t.card
@[simp]
theorem finset.empty_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] (t : finset β) :
@[simp]
theorem finset.empty_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] (t : finset β) :
@[simp]
theorem finset.vadd_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] (s : finset α) :
@[simp]
theorem finset.smul_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] (s : finset α) :
@[simp]
theorem finset.vadd_eq_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset α} {t : finset β} :
s +ᵥ t = s = t =
@[simp]
theorem finset.smul_eq_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset α} {t : finset β} :
s t = s = t =
@[simp]
theorem finset.smul_nonempty_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset α} {t : finset β} :
@[simp]
theorem finset.vadd_nonempty_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset α} {t : finset β} :
theorem finset.nonempty.smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset α} {t : finset β} :
s.nonemptyt.nonempty(s t).nonempty
theorem finset.nonempty.vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset α} {t : finset β} :
s.nonemptyt.nonempty(s +ᵥ t).nonempty
theorem finset.nonempty.of_vadd_left {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset α} {t : finset β} :
(s +ᵥ t).nonempty → s.nonempty
theorem finset.nonempty.of_smul_left {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset α} {t : finset β} :
(s t).nonempty → s.nonempty
theorem finset.nonempty.of_vadd_right {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset α} {t : finset β} :
(s +ᵥ t).nonempty → t.nonempty
theorem finset.nonempty.of_smul_right {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset α} {t : finset β} :
(s t).nonempty → t.nonempty
theorem finset.vadd_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset α} (b : β) :
s +ᵥ {b} = finset.image (λ (_x : α), _x +ᵥ b) s
theorem finset.smul_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset α} (b : β) :
s {b} = finset.image (λ (_x : α), _x b) s
theorem finset.singleton_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {t : finset β} (a : α) :
{a} t =
theorem finset.singleton_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {t : finset β} (a : α) :
{a} +ᵥ t =
@[simp]
theorem finset.singleton_vadd_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] (a : α) (b : β) :
{a} +ᵥ {b} = {a +ᵥ b}
@[simp]
theorem finset.singleton_smul_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] (a : α) (b : β) :
{a} {b} = {a b}
theorem finset.smul_subset_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {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 β] [ β] {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 β] [ β] {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 β] [ β] {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 β] [ β] {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 β] [ β] {s₁ s₂ : finset α} {t : finset β} :
s₁ s₂s₁ t s₂ t
theorem finset.smul_subset_iff {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {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 β] [ β] {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 β] [ β] {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 β] [ β] {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 β] [ β] {s : finset α} {t₁ t₂ : finset β} :
s +ᵥ (t₁ t₂) = s +ᵥ t₁ (s +ᵥ t₂)
theorem finset.smul_union {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {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 β] [ β] {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 β] [ β] {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 β] [ β] {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 β] [ β] {s : finset α} {t₁ t₂ : finset β} :
s +ᵥ t₁ t₂ (s +ᵥ t₁) (s +ᵥ t₂)
theorem finset.subset_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {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 β] [ β] {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 α] [ β] :

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 α] [ β] {s t : finset β} :
s -ᵥ t =
@[simp]
theorem finset.image_vsub_product {α : Type u_2} {β : Type u_3} [decidable_eq α] [ β] {s t : finset β} :
= s -ᵥ t
theorem finset.mem_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [ β] {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 α] [ β] (s t : finset β) :
(s -ᵥ t) = s -ᵥ t
theorem finset.vsub_mem_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [ β] {s t : finset β} {b c : β} :
b sc tb -ᵥ c s -ᵥ t
theorem finset.vsub_card_le {α : Type u_2} {β : Type u_3} [decidable_eq α] [ β] {s t : finset β} :
(s -ᵥ t).card s.card * t.card
@[simp]
theorem finset.empty_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [ β] (t : finset β) :
@[simp]
theorem finset.vsub_empty {α : Type u_2} {β : Type u_3} [decidable_eq α] [ β] (s : finset β) :
@[simp]
theorem finset.vsub_eq_empty {α : Type u_2} {β : Type u_3} [decidable_eq α] [ β] {s t : finset β} :
s -ᵥ t = s = t =
@[simp]
theorem finset.vsub_nonempty {α : Type u_2} {β : Type u_3} [decidable_eq α] [ β] {s t : finset β} :
theorem finset.nonempty.vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [ β] {s t : finset β} :
s.nonemptyt.nonempty(s -ᵥ t).nonempty
theorem finset.nonempty.of_vsub_left {α : Type u_2} {β : Type u_3} [decidable_eq α] [ β] {s t : finset β} :
(s -ᵥ t).nonempty → s.nonempty
theorem finset.nonempty.of_vsub_right {α : Type u_2} {β : Type u_3} [decidable_eq α] [ β] {s t : finset β} :
(s -ᵥ t).nonempty → t.nonempty
@[simp]
theorem finset.vsub_singleton {α : Type u_2} {β : Type u_3} [decidable_eq α] [ β] {s : finset β} (b : β) :
s -ᵥ {b} = finset.image (λ (_x : β), _x -ᵥ b) s
theorem finset.singleton_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [ β] {t : finset β} (a : β) :
{a} -ᵥ t =
@[simp]
theorem finset.singleton_vsub_singleton {α : Type u_2} {β : Type u_3} [decidable_eq α] [ β] (a b : β) :
{a} -ᵥ {b} = {a -ᵥ b}
theorem finset.vsub_subset_vsub {α : Type u_2} {β : Type u_3} [decidable_eq α] [ β] {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 α] [ β] {s t₁ t₂ : finset β} :
t₁ t₂s -ᵥ t₁ s -ᵥ t₂
theorem finset.vsub_subset_vsub_right {α : Type u_2} {β : Type u_3} [decidable_eq α] [ β] {s₁ s₂ t : finset β} :
s₁ s₂s₁ -ᵥ t s₂ -ᵥ t
theorem finset.vsub_subset_iff {α : Type u_2} {β : Type u_3} [decidable_eq α] [ β] {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 α] [ β] {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 α] [ β] {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 α] [ β] {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 α] [ β] {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 α] [ β] {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 β] [ β] :
(finset β)

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 β] [ β] :
(finset β)

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 β] [ β] {s : finset β} {a : α} :
a s =
theorem finset.vadd_finset_def {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset β} {a : α} :
a +ᵥ s =
theorem finset.image_vadd {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset β} {a : α} :
finset.image (λ (x : β), a +ᵥ x) s = a +ᵥ s
theorem finset.image_smul {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset β} {a : α} :
finset.image (λ (x : β), a x) s = a s
theorem finset.mem_smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {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 β] [ β] {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 β] [ β] (a : α) (s : finset β) :
(a s) = a s
@[simp, norm_cast]
theorem finset.coe_vadd_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] (a : α) (s : finset β) :
(a +ᵥ s) = a +ᵥ s
theorem finset.vadd_finset_mem_vadd_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset β} {a : α} {b : β} :
b sa +ᵥ b a +ᵥ s
theorem finset.smul_finset_mem_smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset β} {a : α} {b : β} :
b sa b a s
theorem finset.vadd_finset_card_le {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset β} {a : α} :
(a +ᵥ s).card s.card
theorem finset.smul_finset_card_le {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset β} {a : α} :
(a s).card s.card
@[simp]
theorem finset.vadd_finset_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] (a : α) :
@[simp]
theorem finset.smul_finset_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] (a : α) :
@[simp]
theorem finset.vadd_finset_eq_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset β} {a : α} :
a +ᵥ s = s =
@[simp]
theorem finset.smul_finset_eq_empty {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset β} {a : α} :
a s = s =
@[simp]
theorem finset.vadd_finset_nonempty {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset β} {a : α} :
@[simp]
theorem finset.smul_finset_nonempty {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset β} {a : α} :
theorem finset.nonempty.vadd_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset β} {a : α} (hs : s.nonempty) :
theorem finset.nonempty.smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s : finset β} {a : α} (hs : s.nonempty) :
theorem finset.vadd_finset_subset_vadd_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s t : finset β} {a : α} :
s ta +ᵥ s a +ᵥ t
theorem finset.smul_finset_subset_smul_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s t : finset β} {a : α} :
s ta s a t
@[simp]
theorem finset.smul_finset_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {a : α} (b : β) :
a {b} = {a b}
@[simp]
theorem finset.vadd_finset_singleton {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {a : α} (b : β) :
a +ᵥ {b} = {a +ᵥ b}
theorem finset.vadd_finset_union {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {s₁ s₂ : finset β} {a : α} :
a +ᵥ (s₁ s₂) = a +ᵥ s₁ (a +ᵥ s₂)
theorem finset.smul_finset_union {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] {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 β] [ β] {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 β] [ β] {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 β] [ β] (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 γ] [ γ] [ γ] [ γ] :
(finset γ)
@[protected, instance]
def finset.smul_comm_class_finset {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [ γ] [ γ] [ γ] :
(finset γ)
@[protected, instance]
def finset.vadd_comm_class_finset' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [ γ] [ γ] [ γ] :
(finset β) (finset γ)
@[protected, instance]
def finset.smul_comm_class_finset' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [ γ] [ γ] [ γ] :
(finset β) (finset γ)
@[protected, instance]
def finset.vadd_comm_class_finset'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [ γ] [ γ] [ γ] :
β (finset γ)
@[protected, instance]
def finset.smul_comm_class_finset'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [ γ] [ γ] [ γ] :
β (finset γ)
@[protected, instance]
def finset.vadd_comm_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [ γ] [ γ] [ γ] :
(finset β) (finset γ)
@[protected, instance]
def finset.smul_comm_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [ γ] [ γ] [ γ] :
(finset β) (finset γ)
@[protected, instance]
def finset.is_scalar_tower {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [ β] [ γ] [ γ] [ γ] :
(finset γ)
@[protected, instance]
def finset.vadd_assoc_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [ β] [ γ] [ γ] [ γ] :
(finset γ)
@[protected, instance]
def finset.is_scalar_tower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [decidable_eq β] [ β] [ γ] [ γ] [ γ] :
(finset β) (finset γ)
@[protected, instance]
def finset.vadd_assoc_class' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [decidable_eq β] [ β] [ γ] [ γ] [ γ] :
(finset β) (finset γ)
@[protected, instance]
def finset.vadd_assoc_class'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [decidable_eq β] [ β] [ γ] [ γ] [ γ] :
(finset β) (finset γ)
@[protected, instance]
def finset.is_scalar_tower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [decidable_eq γ] [decidable_eq β] [ β] [ γ] [ γ] [ γ] :
(finset β) (finset γ)
@[protected, instance]
def finset.is_central_scalar {α : Type u_2} {β : Type u_3} [decidable_eq β] [ β] [ β] [ β] :
(finset β)
@[protected]
def finset.mul_action {α : Type u_2} {β : Type u_3} [decidable_eq β] [decidable_eq α] [monoid α] [ β] :

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 α] [ β] :

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

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

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 β] [ β] :
(finset β)

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 β]  :

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

Equations
@[protected, instance]
def finset.no_zero_divisors {α : Type u_2} [decidable_eq α] [has_zero α] [has_mul α]  :
@[protected, instance]
def finset.no_zero_smul_divisors {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_zero α] [has_zero β] [ β]  :
(finset β)
@[protected, instance]
def finset.no_zero_smul_divisors_finset {α : Type u_2} {β : Type u_3} [decidable_eq β] [has_zero α] [has_zero β] [ β]  :
theorem finset.pairwise_disjoint_smul_iff {α : Type u_2} [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} [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} [decidable_eq α] (t : finset α) (a : α) :
({a} + t).card = t.card
@[simp]
theorem finset.card_singleton_mul {α : Type u_2} [decidable_eq α] (t : finset α) (a : α) :
({a} * t).card = t.card
theorem finset.singleton_mul_inter {α : Type u_2} [decidable_eq α] (s t : finset α) (a : α) :
{a} * (s t) = {a} * s ({a} * t)
theorem finset.singleton_add_inter {α : Type u_2} [decidable_eq α] (s t : finset α) (a : α) :
{a} + s t = ({a} + s) ({a} + t)
theorem finset.card_le_card_add_left {α : Type u_2} [decidable_eq α] (t : finset α) {s : finset α} (hs : s.nonempty) :
t.card (s + t).card
theorem finset.card_le_card_mul_left {α : Type u_2} [decidable_eq α] (t : finset α) {s : finset α} (hs : s.nonempty) :
t.card (s * t).card
@[simp]
theorem finset.card_add_singleton {α : Type u_2} [decidable_eq α] (s : finset α) (a : α) :
(s + {a}).card = s.card
@[simp]
theorem finset.card_mul_singleton {α : Type u_2} [decidable_eq α] (s : finset α) (a : α) :
(s * {a}).card = s.card
theorem finset.inter_add_singleton {α : Type u_2} [decidable_eq α] (s t : finset α) (a : α) :
s t + {a} = (s + {a}) (t + {a})
theorem finset.inter_mul_singleton {α : Type u_2} [decidable_eq α] (s t : finset α) (a : α) :
s t * {a} = s * {a} (t * {a})
theorem finset.card_le_card_add_right {α : Type u_2} [decidable_eq α] (s : finset α) {t : finset α} (ht : t.nonempty) :
s.card (s + t).card
theorem finset.card_le_card_mul_right {α : Type u_2} [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 α] [ β] {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 α] [ β] {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 α] [ β] {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 α] [ β] {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 α] [ β] {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 α] [ β] {s : finset β} {a : α} {b : β} :
b