# mathlibdocumentation

algebra.pointwise

# Pointwise addition, multiplication, and scalar multiplication of sets. #

This file defines pointwise algebraic operations on sets.

• For a type `α` with multiplication, multiplication is defined on `set α` by taking `s * t` to be the set of all `x * y` where `x ∈ s` and `y ∈ t`. Similarly for addition.
• For `α` a semigroup, `set α` is a semigroup.
• If `α` is a (commutative) monoid, we define an alias `set_semiring α` for `set α`, which then becomes a (commutative) semiring with union as addition and pointwise multiplication as multiplication.
• For a type `β` with scalar multiplication by another type `α`, this file defines a scalar multiplication of `set β` by `set α` and a separate scalar multiplication of `set β` by `α`.
• We also define pointwise multiplication on `finset`.

Appropriate definitions and results are also transported to the additive theory via `to_additive`.

## Implementation notes #

• The following expressions are considered in simp-normal form in a group: `(λ h, h * g) ⁻¹' s`, `(λ h, g * h) ⁻¹' s`, `(λ h, h * g⁻¹) ⁻¹' s`, `(λ h, g⁻¹ * h) ⁻¹' s`, `s * t`, `s⁻¹`, `(1 : set _)` (and similarly for additive variants). Expressions equal to one of these will be simplified.
• 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 #

@[protected, instance]
def set.has_one {α : Type u_1} [has_one α] :

The set `(1 : set α)` is defined as `{1}` in locale `pointwise`.

Equations
@[protected, instance]
def set.has_zero {α : Type u_1} [has_zero α] :

The set `(0 : set α)` is defined as `{0}` in locale `pointwise`.

Equations
theorem set.singleton_one {α : Type u_1} [has_one α] :
{1} = 1
theorem set.singleton_zero {α : Type u_1} [has_zero α] :
{0} = 0
@[simp]
theorem set.mem_one {α : Type u_1} {a : α} [has_one α] :
a 1 a = 1
@[simp]
theorem set.mem_zero {α : Type u_1} {a : α} [has_zero α] :
a 0 a = 0
theorem set.zero_mem_zero {α : Type u_1} [has_zero α] :
0 0
theorem set.one_mem_one {α : Type u_1} [has_one α] :
1 1
@[simp]
theorem set.zero_subset {α : Type u_1} {s : set α} [has_zero α] :
0 s 0 s
@[simp]
theorem set.one_subset {α : Type u_1} {s : set α} [has_one α] :
1 s 1 s
theorem set.zero_nonempty {α : Type u_1} [has_zero α] :
theorem set.one_nonempty {α : Type u_1} [has_one α] :
@[simp]
theorem set.image_zero {α : Type u_1} {β : Type u_2} [has_zero α] {f : α → β} :
f '' 0 = {f 0}
@[simp]
theorem set.image_one {α : Type u_1} {β : Type u_2} [has_one α] {f : α → β} :
f '' 1 = {f 1}

@[protected, instance]
def set.has_mul {α : Type u_1} [has_mul α] :

The set `(s * t : set α)` is defined as `{x * y | x ∈ s, y ∈ t}` in locale `pointwise`.

Equations
@[protected, instance]

The set `(s + t : set α)` is defined as `{x + y | x ∈ s, y ∈ t}` in locale `pointwise`.

Equations
@[simp]
theorem set.image2_mul {α : Type u_1} {s t : set α} [has_mul α] :
= s * t
@[simp]
theorem set.image2_add {α : Type u_1} {s t : set α} [has_add α] :
= s + t
theorem set.mem_add {α : Type u_1} {s t : set α} {a : α} [has_add α] :
a s + t ∃ (x y : α), x s y t x + y = a
theorem set.mem_mul {α : Type u_1} {s t : set α} {a : α} [has_mul α] :
a s * t ∃ (x y : α), x s y t x * y = a
theorem set.mul_mem_mul {α : Type u_1} {s t : set α} {a b : α} [has_mul α] (ha : a s) (hb : b t) :
a * b s * t
theorem set.add_mem_add {α : Type u_1} {s t : set α} {a b : α} [has_add α] (ha : a s) (hb : b t) :
a + b s + t
theorem set.image_mul_prod {α : Type u_1} {s t : set α} [has_mul α] :
(λ (x : α × α), (x.fst) * x.snd) '' (s ×ˢ t) = s * t
theorem set.add_image_prod {α : Type u_1} {s t : set α} [has_add α] :
(λ (x : α × α), x.fst + x.snd) '' (s ×ˢ t) = s + t
@[simp]
theorem set.image_add_left {α : Type u_1} {t : set α} {a : α} [add_group α] :
(λ (b : α), a + b) '' t = (λ (b : α), -a + b) ⁻¹' t
@[simp]
theorem set.image_mul_left {α : Type u_1} {t : set α} {a : α} [group α] :
(λ (b : α), a * b) '' t = (λ (b : α), a⁻¹ * b) ⁻¹' t
@[simp]
theorem set.image_mul_right {α : Type u_1} {t : set α} {b : α} [group α] :
(λ (a : α), a * b) '' t = (λ (a : α), a * b⁻¹) ⁻¹' t
@[simp]
theorem set.image_add_right {α : Type u_1} {t : set α} {b : α} [add_group α] :
(λ (a : α), a + b) '' t = (λ (a : α), a + -b) ⁻¹' t
theorem set.image_mul_left' {α : Type u_1} {t : set α} {a : α} [group α] :
(λ (b : α), a⁻¹ * b) '' t = (λ (b : α), a * b) ⁻¹' t
theorem set.image_add_left' {α : Type u_1} {t : set α} {a : α} [add_group α] :
(λ (b : α), -a + b) '' t = (λ (b : α), a + b) ⁻¹' t
theorem set.image_mul_right' {α : Type u_1} {t : set α} {b : α} [group α] :
(λ (a : α), a * b⁻¹) '' t = (λ (a : α), a * b) ⁻¹' t
theorem set.image_add_right' {α : Type u_1} {t : set α} {b : α} [add_group α] :
(λ (a : α), a + -b) '' t = (λ (a : α), a + b) ⁻¹' t
@[simp]
theorem set.preimage_mul_left_singleton {α : Type u_1} {a b : α} [group α] :
⁻¹' {b} = {a⁻¹ * b}
@[simp]
theorem set.preimage_add_left_singleton {α : Type u_1} {a b : α} [add_group α] :
⁻¹' {b} = {-a + b}
@[simp]
theorem set.preimage_mul_right_singleton {α : Type u_1} {a b : α} [group α] :
(λ (_x : α), _x * a) ⁻¹' {b} = {b * a⁻¹}
@[simp]
theorem set.preimage_add_right_singleton {α : Type u_1} {a b : α} [add_group α] :
(λ (_x : α), _x + a) ⁻¹' {b} = {b + -a}
@[simp]
theorem set.preimage_mul_left_one {α : Type u_1} {a : α} [group α] :
(λ (b : α), a * b) ⁻¹' 1 = {a⁻¹}
@[simp]
theorem set.preimage_add_left_zero {α : Type u_1} {a : α} [add_group α] :
(λ (b : α), a + b) ⁻¹' 0 = {-a}
@[simp]
theorem set.preimage_add_right_zero {α : Type u_1} {b : α} [add_group α] :
(λ (a : α), a + b) ⁻¹' 0 = {-b}
@[simp]
theorem set.preimage_mul_right_one {α : Type u_1} {b : α} [group α] :
(λ (a : α), a * b) ⁻¹' 1 = {b⁻¹}
theorem set.preimage_add_left_zero' {α : Type u_1} {a : α} [add_group α] :
(λ (b : α), -a + b) ⁻¹' 0 = {a}
theorem set.preimage_mul_left_one' {α : Type u_1} {a : α} [group α] :
(λ (b : α), a⁻¹ * b) ⁻¹' 1 = {a}
theorem set.preimage_add_right_zero' {α : Type u_1} {b : α} [add_group α] :
(λ (a : α), a + -b) ⁻¹' 0 = {b}
theorem set.preimage_mul_right_one' {α : Type u_1} {b : α} [group α] :
(λ (a : α), a * b⁻¹) ⁻¹' 1 = {b}
@[simp]
theorem set.add_singleton {α : Type u_1} {s : set α} {b : α} [has_add α] :
s + {b} = (λ (a : α), a + b) '' s
@[simp]
theorem set.mul_singleton {α : Type u_1} {s : set α} {b : α} [has_mul α] :
s * {b} = (λ (a : α), a * b) '' s
@[simp]
theorem set.singleton_add {α : Type u_1} {t : set α} {a : α} [has_add α] :
{a} + t = (λ (b : α), a + b) '' t
@[simp]
theorem set.singleton_mul {α : Type u_1} {t : set α} {a : α} [has_mul α] :
{a} * t = (λ (b : α), a * b) '' t
@[simp]
theorem set.singleton_mul_singleton {α : Type u_1} {a b : α} [has_mul α] :
{a} * {b} = {a * b}
@[simp]
theorem set.singleton_add_singleton {α : Type u_1} {a b : α} [has_add α] :
{a} + {b} = {a + b}
@[protected]
theorem set.mul_comm {α : Type u_1} {s t : set α}  :
s * t = t * s
@[protected]
theorem set.add_comm {α : Type u_1} {s t : set α}  :
s + t = t + s
@[protected, instance]
def set.add_zero_class {α : Type u_1}  :

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

Equations
@[protected, instance]
def set.mul_one_class {α : Type u_1}  :

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

Equations
@[protected, instance]
def set.add_semigroup {α : Type u_1}  :

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

Equations
@[protected, instance]
def set.semigroup {α : Type u_1} [semigroup α] :

`set α` is a `semigroup` under pointwise operations if `α` is.

Equations
@[protected, instance]
def set.monoid {α : Type u_1} [monoid α] :
monoid (set α)

`set α` is a `monoid` under pointwise operations if `α` is.

Equations
@[protected, instance]

`set α` is an `add_monoid` under pointwise operations if `α` is.

Equations
@[protected, instance]
def set.comm_monoid {α : Type u_1} [comm_monoid α] :

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

Equations
@[protected, instance]
def set.add_comm_monoid {α : Type u_1}  :

`set α` is an `add_comm_monoid` under pointwise operations if `α` is.

Equations
theorem set.nsmul_mem_nsmul {α : Type u_1} {s : set α} {a : α} [add_monoid α] (ha : a s) (n : ) :
n a n s
theorem set.pow_mem_pow {α : Type u_1} {s : set α} {a : α} [monoid α] (ha : a s) (n : ) :
a ^ n s ^ n
def set.singleton_mul_hom {α : Type u_1} [has_mul α] :
(set α)

Under `[has_mul M]`, the `singleton` map from `M` to `set M` as a `mul_hom`, that is, a map which preserves multiplication.

Equations
@[simp]
theorem set.singleton_add_hom_apply {α : Type u_1} [has_add α] (ᾰ : α) :
(set α)

Under `[has_add A]`, the `singleton` map from `A` to `set A` as an `add_hom`, that is, a map which preserves addition.

Equations
@[simp]
theorem set.singleton_mul_hom_apply {α : Type u_1} [has_mul α] (ᾰ : α) :
@[simp]
theorem set.empty_mul {α : Type u_1} {s : set α} [has_mul α] :
@[simp]
theorem set.empty_add {α : Type u_1} {s : set α} [has_add α] :
@[simp]
theorem set.add_empty {α : Type u_1} {s : set α} [has_add α] :
@[simp]
theorem set.mul_empty {α : Type u_1} {s : set α} [has_mul α] :
theorem set.empty_pow {α : Type u_1} [monoid α] (n : ) (hn : n 0) :
theorem set.empty_smul {α : Type u_1} [add_monoid α] (n : ) (hn : n 0) :
@[protected, instance]
def set.decidable_mem_mul {α : Type u_1} {s t : set α} [monoid α] [fintype α] [decidable_eq α] [decidable_pred (λ (_x : α), _x s)] [decidable_pred (λ (_x : α), _x t)] :
decidable_pred (λ (_x : α), _x s * t)
Equations
@[protected, instance]
def set.decidable_mem_pow {α : Type u_1} {s : set α} [monoid α] [fintype α] [decidable_eq α] [decidable_pred (λ (_x : α), _x s)] (n : ) :
decidable_pred (λ (_x : α), _x s ^ n)
Equations
• = nat.rec (set.decidable_mem_pow._proof_1.mpr (set.decidable_mem_pow._proof_2.mpr (λ (a : α), _inst_3 a 1))) (λ (n : ) (ih : decidable_pred (λ (_x : α), _x s ^ n)), let _inst : decidable_pred (λ (_x : α), _x s ^ n) := ih in _.mpr (λ (a : α), n
theorem set.add_subset_add {α : Type u_1} {s₁ s₂ t₁ t₂ : set α} [has_add α] (h₁ : s₁ t₁) (h₂ : s₂ t₂) :
s₁ + s₂ t₁ + t₂
theorem set.mul_subset_mul {α : Type u_1} {s₁ s₂ t₁ t₂ : set α} [has_mul α] (h₁ : s₁ t₁) (h₂ : s₂ t₂) :
s₁ * s₂ t₁ * t₂
theorem set.add_subset_add_left {α : Type u_1} {s t₁ t₂ : set α} [has_add α] (h : t₁ t₂) :
s + t₁ s + t₂
theorem set.mul_subset_mul_left {α : Type u_1} {s t₁ t₂ : set α} [has_mul α] (h : t₁ t₂) :
s * t₁ s * t₂
theorem set.mul_subset_mul_right {α : Type u_1} {s₁ s₂ t : set α} [has_mul α] (h : s₁ s₂) :
s₁ * t s₂ * t
theorem set.add_subset_add_right {α : Type u_1} {s₁ s₂ t : set α} [has_add α] (h : s₁ s₂) :
s₁ + t s₂ + t
theorem set.pow_subset_pow {α : Type u_1} {s t : set α} [monoid α] (hst : s t) (n : ) :
s ^ n t ^ n
theorem set.union_mul {α : Type u_1} {s t u : set α} [has_mul α] :
(s t) * u = s * u t * u
theorem set.union_add {α : Type u_1} {s t u : set α} [has_add α] :
s t + u = s + u (t + u)
theorem set.mul_union {α : Type u_1} {s t u : set α} [has_mul α] :
s * (t u) = s * t s * u
theorem set.add_union {α : Type u_1} {s t u : set α} [has_add α] :
s + (t u) = s + t (s + u)
theorem set.Union_mul_left_image {α : Type u_1} {s t : set α} [has_mul α] :
(⋃ (a : α) (H : a s), (λ (x : α), a * x) '' t) = s * t
theorem set.Union_add_left_image {α : Type u_1} {s t : set α} [has_add α] :
(⋃ (a : α) (H : a s), (λ (x : α), a + x) '' t) = s + t
theorem set.Union_mul_right_image {α : Type u_1} {s t : set α} [has_mul α] :
(⋃ (a : α) (H : a t), (λ (x : α), x * a) '' s) = s * t
theorem set.Union_add_right_image {α : Type u_1} {s t : set α} [has_add α] :
(⋃ (a : α) (H : a t), (λ (x : α), x + a) '' s) = s + t
theorem set.Union_add {α : Type u_1} {ι : Sort u_2} [has_add α] (s : ι → set α) (t : set α) :
(⋃ (i : ι), s i) + t = ⋃ (i : ι), s i + t
theorem set.Union_mul {α : Type u_1} {ι : Sort u_2} [has_mul α] (s : ι → set α) (t : set α) :
(⋃ (i : ι), s i) * t = ⋃ (i : ι), (s i) * t
theorem set.add_Union {α : Type u_1} {ι : Sort u_2} [has_add α] (t : set α) (s : ι → set α) :
(t + ⋃ (i : ι), s i) = ⋃ (i : ι), t + s i
theorem set.mul_Union {α : Type u_1} {ι : Sort u_2} [has_mul α] (t : set α) (s : ι → set α) :
(t * ⋃ (i : ι), s i) = ⋃ (i : ι), t * s i
@[simp]
@[simp]
theorem set.univ_mul_univ {α : Type u_1} [monoid α] :
def set.singleton_hom {α : Type u_1} [monoid α] :
α →* set α

`singleton` is a monoid hom.

Equations
theorem set.nonempty.add {α : Type u_1} {s t : set α} [has_add α] :
s.nonemptyt.nonempty(s + t).nonempty
theorem set.nonempty.mul {α : Type u_1} {s t : set α} [has_mul α] :
s.nonemptyt.nonempty(s * t).nonempty
theorem set.finite.mul {α : Type u_1} {s t : set α} [has_mul α] (hs : s.finite) (ht : t.finite) :
(s * t).finite
theorem set.finite.add {α : Type u_1} {s t : set α} [has_add α] (hs : s.finite) (ht : t.finite) :
(s + t).finite
def set.fintype_add {α : Type u_1} [has_add α] [decidable_eq α] (s t : set α) [hs : fintype s] [ht : fintype t] :

Equations
def set.fintype_mul {α : Type u_1} [has_mul α] [decidable_eq α] (s t : set α) [hs : fintype s] [ht : fintype t] :

multiplication preserves finiteness

Equations
theorem set.bdd_above_add {α : Type u_1} {A B : set α} :
bdd_above (A + B)
theorem set.bdd_above_mul {α : Type u_1} {A B : set α} :
bdd_above (A * B)
theorem set.mem_finset_sum {α : Type u_1} {ι : Type u_4} (t : finset ι) (f : ι → set α) (a : α) :
a ∑ (i : ι) in t, f i ∃ (g : ι → α) (hg : ∀ {i : ι}, i tg i f i), ∑ (i : ι) in t, g i = a

The n-ary version of `set.mem_add`.

theorem set.mem_finset_prod {α : Type u_1} {ι : Type u_4} [comm_monoid α] (t : finset ι) (f : ι → set α) (a : α) :
a ∏ (i : ι) in t, f i ∃ (g : ι → α) (hg : ∀ {i : ι}, i tg i f i), ∏ (i : ι) in t, g i = a

The n-ary version of `set.mem_mul`.

theorem set.mem_fintype_prod {α : Type u_1} {ι : Type u_4} [comm_monoid α] [fintype ι] (f : ι → set α) (a : α) :
a ∏ (i : ι), f i ∃ (g : ι → α) (hg : ∀ (i : ι), g i f i), ∏ (i : ι), g i = a

A version of `set.mem_finset_prod` with a simpler RHS for products over a fintype.

theorem set.mem_fintype_sum {α : Type u_1} {ι : Type u_4} [fintype ι] (f : ι → set α) (a : α) :
a ∑ (i : ι), f i ∃ (g : ι → α) (hg : ∀ (i : ι), g i f i), ∑ (i : ι), g i = a

A version of `set.mem_finset_sum` with a simpler RHS for sums over a fintype.

theorem set.finset_prod_mem_finset_prod {α : Type u_1} {ι : Type u_4} [comm_monoid α] (t : finset ι) (f : ι → set α) (g : ι → α) (hg : ∀ (i : ι), i tg i f i) :
∏ (i : ι) in t, g i ∏ (i : ι) in t, f i

The n-ary version of `set.mul_mem_mul`.

theorem set.finset_sum_mem_finset_sum {α : Type u_1} {ι : Type u_4} (t : finset ι) (f : ι → set α) (g : ι → α) (hg : ∀ (i : ι), i tg i f i) :
∑ (i : ι) in t, g i ∑ (i : ι) in t, f i

The n-ary version of `set.add_mem_add`.

theorem set.finset_prod_subset_finset_prod {α : Type u_1} {ι : Type u_4} [comm_monoid α] (t : finset ι) (f₁ f₂ : ι → set α) (hf : ∀ {i : ι}, i tf₁ i f₂ i) :
∏ (i : ι) in t, f₁ i ∏ (i : ι) in t, f₂ i

The n-ary version of `set.mul_subset_mul`.

theorem set.finset_sum_subset_finset_sum {α : Type u_1} {ι : Type u_4} (t : finset ι) (f₁ f₂ : ι → set α) (hf : ∀ {i : ι}, i tf₁ i f₂ i) :
∑ (i : ι) in t, f₁ i ∑ (i : ι) in t, f₂ i

The n-ary version of `set.add_subset_add`.

theorem set.finset_prod_singleton {M : Type u_1} {ι : Type u_2} [comm_monoid M] (s : finset ι) (I : ι → M) :
∏ (i : ι) in s, {I i} = {∏ (i : ι) in s, I i}
theorem set.finset_sum_singleton {M : Type u_1} {ι : Type u_2} (s : finset ι) (I : ι → M) :
∑ (i : ι) in s, {I i} = {∑ (i : ι) in s, I i}

TODO: define `decidable_mem_finset_prod` and `decidable_mem_finset_sum`.

@[protected, instance]
def set.has_neg {α : Type u_1} [has_neg α] :

The set `(-s : set α)` is defined as `{x | -x ∈ s}` in locale `pointwise`. It is equal to `{-x | x ∈ s}`, see `set.image_neg`.

Equations
@[protected, instance]
def set.has_inv {α : Type u_1} [has_inv α] :

The set `(s⁻¹ : set α)` is defined as `{x | x⁻¹ ∈ s}` in locale `pointwise`. It is equal to `{x⁻¹ | x ∈ s}`, see `set.image_inv`.

Equations
@[simp]
theorem set.neg_empty {α : Type u_1} [has_neg α] :
@[simp]
theorem set.inv_empty {α : Type u_1} [has_inv α] :
@[simp]
theorem set.neg_univ {α : Type u_1} [has_neg α] :
@[simp]
theorem set.inv_univ {α : Type u_1} [has_inv α] :
@[simp]
theorem set.nonempty_neg {α : Type u_1} [add_group α] {s : set α} :
@[simp]
theorem set.nonempty_inv {α : Type u_1} [group α] {s : set α} :
theorem set.nonempty.inv {α : Type u_1} [group α] {s : set α} (h : s.nonempty) :
theorem set.nonempty.neg {α : Type u_1} [add_group α] {s : set α} (h : s.nonempty) :
@[simp]
theorem set.mem_inv {α : Type u_1} {s : set α} {a : α} [has_inv α] :
@[simp]
theorem set.mem_neg {α : Type u_1} {s : set α} {a : α} [has_neg α] :
a -s -a s
theorem set.inv_mem_inv {α : Type u_1} {s : set α} {a : α} [group α] :
theorem set.neg_mem_neg {α : Type u_1} {s : set α} {a : α} [add_group α] :
-a -s a s
@[simp]
theorem set.inv_preimage {α : Type u_1} {s : set α} [has_inv α] :
@[simp]
theorem set.neg_preimage {α : Type u_1} {s : set α} [has_neg α] :
= -s
@[simp]
theorem set.image_inv {α : Type u_1} {s : set α} [group α] :
@[simp]
theorem set.image_neg {α : Type u_1} {s : set α} [add_group α] :
= -s
@[simp]
theorem set.inter_neg {α : Type u_1} {s t : set α} [has_neg α] :
-(s t) = -s -t
@[simp]
theorem set.inter_inv {α : Type u_1} {s t : set α} [has_inv α] :
@[simp]
theorem set.union_neg {α : Type u_1} {s t : set α} [has_neg α] :
-(s t) = -s -t
@[simp]
theorem set.union_inv {α : Type u_1} {s t : set α} [has_inv α] :
@[simp]
theorem set.Inter_inv {α : Type u_1} {ι : Sort u_2} [has_inv α] (s : ι → set α) :
(⋂ (i : ι), s i)⁻¹ = ⋂ (i : ι), (s i)⁻¹
@[simp]
theorem set.Inter_neg {α : Type u_1} {ι : Sort u_2} [has_neg α] (s : ι → set α) :
(-⋂ (i : ι), s i) = ⋂ (i : ι), -s i
@[simp]
theorem set.Union_inv {α : Type u_1} {ι : Sort u_2} [has_inv α] (s : ι → set α) :
(⋃ (i : ι), s i)⁻¹ = ⋃ (i : ι), (s i)⁻¹
@[simp]
theorem set.Union_neg {α : Type u_1} {ι : Sort u_2} [has_neg α] (s : ι → set α) :
(-⋃ (i : ι), s i) = ⋃ (i : ι), -s i
@[simp]
theorem set.compl_neg {α : Type u_1} {s : set α} [has_neg α] :
-s = (-s)
@[simp]
theorem set.compl_inv {α : Type u_1} {s : set α} [has_inv α] :
@[protected, simp]
theorem set.neg_neg {α : Type u_1} {s : set α} [add_group α] :
--s = s
@[protected, simp]
theorem set.inv_inv {α : Type u_1} {s : set α} [group α] :
@[protected, simp]
theorem set.univ_neg {α : Type u_1} [add_group α] :
@[protected, simp]
theorem set.univ_inv {α : Type u_1} [group α] :
@[simp]
theorem set.neg_subset_neg {α : Type u_1} [add_group α] {s t : set α} :
-s -t s t
@[simp]
theorem set.inv_subset_inv {α : Type u_1} [group α] {s t : set α} :
theorem set.inv_subset {α : Type u_1} [group α] {s t : set α} :
theorem set.neg_subset {α : Type u_1} [add_group α] {s t : set α} :
-s t s -t
theorem set.finite.inv {α : Type u_1} [group α] {s : set α} (hs : s.finite) :
theorem set.finite.neg {α : Type u_1} [add_group α] {s : set α} (hs : s.finite) :
theorem set.inv_singleton {β : Type u_1} [group β] (x : β) :
{x}⁻¹ = {x⁻¹}
theorem set.neg_singleton {β : Type u_1} [add_group β] (x : β) :
-{x} = {-x}
@[protected]
theorem set.add_neg_rev {α : Type u_1} [add_group α] (s t : set α) :
-(s + t) = -t + -s
@[protected]
theorem set.mul_inv_rev {α : Type u_1} [group α] (s t : set α) :
(s * t)⁻¹ = t⁻¹ * s⁻¹

### Properties about scalar multiplication #

@[protected, instance]
def set.has_vadd_set {α : Type u_1} {β : Type u_2} [ β] :
(set β)

The translation of a set `(x +ᵥ s : set β)` by a scalar `x ∶ α` is defined as `{x +ᵥ y | y ∈ s}` in locale `pointwise`.

Equations
@[protected, instance]
def set.has_scalar_set {α : Type u_1} {β : Type u_2} [ β] :
(set β)

The scaling of a set `(x • s : set β)` by a scalar `x ∶ α` is defined as `{x • y | y ∈ s}` in locale `pointwise`.

Equations
@[protected, instance]
def set.has_scalar {α : Type u_1} {β : Type u_2} [ β] :
has_scalar (set α) (set β)

The pointwise scalar multiplication `(s • t : set β)` by a set of scalars `s ∶ set α` is defined as `{x • y | x ∈ s, y ∈ t}` in locale `pointwise`.

Equations
@[protected, instance]
def set.has_vadd {α : Type u_1} {β : Type u_2} [ β] :

The pointwise translation `(s +ᵥ t : set β)` by a set of constants `s ∶ set α` is defined as `{x +ᵥ y | x ∈ s, y ∈ t}` in locale `pointwise`.

Equations
@[simp]
theorem set.image_vadd {α : Type u_1} {β : Type u_2} {a : α} [ β] {t : set β} :
(λ (x : β), a +ᵥ x) '' t = a +ᵥ t
@[simp]
theorem set.image_smul {α : Type u_1} {β : Type u_2} {a : α} [ β] {t : set β} :
(λ (x : β), a x) '' t = a t
theorem set.mem_vadd_set {α : Type u_1} {β : Type u_2} {a : α} {x : β} [ β] {t : set β} :
x a +ᵥ t ∃ (y : β), y t a +ᵥ y = x
theorem set.mem_smul_set {α : Type u_1} {β : Type u_2} {a : α} {x : β} [ β] {t : set β} :
x a t ∃ (y : β), y t a y = x
theorem set.smul_mem_smul_set {α : Type u_1} {β : Type u_2} {a : α} {y : β} [ β] {t : set β} (hy : y t) :
a y a t
theorem set.vadd_mem_vadd_set {α : Type u_1} {β : Type u_2} {a : α} {y : β} [ β] {t : set β} (hy : y t) :
a +ᵥ y a +ᵥ t
theorem set.vadd_set_union {α : Type u_1} {β : Type u_2} {a : α} [ β] {s t : set β} :
a +ᵥ (s t) = a +ᵥ s (a +ᵥ t)
theorem set.smul_set_union {α : Type u_1} {β : Type u_2} {a : α} [ β] {s t : set β} :
a (s t) = a s a t
theorem set.vadd_set_inter {α : Type u_1} {β : Type u_2} {a : α} [add_group α] [ β] {s t : set β} :
a +ᵥ s t = (a +ᵥ s) (a +ᵥ t)
theorem set.smul_set_inter {α : Type u_1} {β : Type u_2} {a : α} [group α] [ β] {s t : set β} :
a (s t) = a s a t
theorem set.smul_set_inter₀ {α : Type u_1} {β : Type u_2} {a : α} [ β] {s t : set β} (ha : a 0) :
a (s t) = a s a t
theorem set.smul_set_inter_subset {α : Type u_1} {β : Type u_2} {a : α} [ β] {s t : set β} :
a (s t) a s a t
theorem set.vadd_set_inter_subset {α : Type u_1} {β : Type u_2} {a : α} [ β] {s t : set β} :
a +ᵥ s t (a +ᵥ s) (a +ᵥ t)
@[simp]
theorem set.smul_set_empty {α : Type u_1} {β : Type u_2} [ β] (a : α) :
@[simp]
theorem set.vadd_set_empty {α : Type u_1} {β : Type u_2} [ β] (a : α) :
theorem set.vadd_set_mono {α : Type u_1} {β : Type u_2} {a : α} [ β] {s t : set β} (h : s t) :
a +ᵥ s a +ᵥ t
theorem set.smul_set_mono {α : Type u_1} {β : Type u_2} {a : α} [ β] {s t : set β} (h : s t) :
a s a t
@[simp]
theorem set.image2_smul {α : Type u_1} {β : Type u_2} {s : set α} [ β] {t : set β} :
= s t
@[simp]
theorem set.image2_vadd {α : Type u_1} {β : Type u_2} {s : set α} [ β] {t : set β} :
= s +ᵥ t
theorem set.mem_vadd {α : Type u_1} {β : Type u_2} {s : set α} {x : β} [ β] {t : set β} :
x s +ᵥ t ∃ (a : α) (y : β), a s y t a +ᵥ y = x
theorem set.mem_smul {α : Type u_1} {β : Type u_2} {s : set α} {x : β} [ β] {t : set β} :
x s t ∃ (a : α) (y : β), a s y t a y = x
theorem set.mem_smul_of_mem {α : Type u_1} {β : Type u_2} {s : set α} [ β] {t : set β} {a : α} {b : β} (ha : a s) (hb : b t) :
a b s t
theorem set.image_vadd_sum {α : Type u_1} {β : Type u_2} {s : set α} [ β] {t : set β} :
(λ (x : α × β), x.fst +ᵥ x.snd) '' (s ×ˢ t) = s +ᵥ t
theorem set.image_smul_prod {α : Type u_1} {β : Type u_2} {s : set α} [ β] {t : set β} :
(λ (x : α × β), x.fst x.snd) '' (s ×ˢ t) = s t
theorem set.range_vadd_range {α : Type u_1} {β : Type u_2} {ι : Type u_4} {κ : Type u_5} [ β] (b : ι → α) (c : κ → β) :
= set.range (λ (p : ι × κ), b p.fst +ᵥ c p.snd)
theorem set.range_smul_range {α : Type u_1} {β : Type u_2} {ι : Type u_4} {κ : Type u_5} [ β] (b : ι → α) (c : κ → β) :
= set.range (λ (p : ι × κ), b p.fst c p.snd)
@[simp]
theorem set.vadd_singleton {α : Type u_1} {β : Type u_2} [ β] (a : α) (b : β) :
a +ᵥ {b} = {a +ᵥ b}
@[simp]
theorem set.smul_singleton {α : Type u_1} {β : Type u_2} [ β] (a : α) (b : β) :
a {b} = {a b}
@[simp]
theorem set.singleton_smul {α : Type u_1} {β : Type u_2} {a : α} [ β] {t : set β} :
{a} t = a t
@[simp]
theorem set.singleton_vadd {α : Type u_1} {β : Type u_2} {a : α} [ β] {t : set β} :
{a} +ᵥ t = a +ᵥ t
@[protected, instance]
def set.vadd_comm_class_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ γ] [ γ] [ γ] :
(set β) (set γ)
@[protected, instance]
def set.smul_comm_class_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ γ] [ γ] [ γ] :
(set β) (set γ)
@[protected, instance]
def set.vadd_comm_class_set' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ γ] [ γ] [ γ] :
β (set γ)
@[protected, instance]
def set.smul_comm_class_set' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ γ] [ γ] [ γ] :
β (set γ)
@[protected, instance]
def set.vadd_comm_class {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ γ] [ γ] [ γ] :
(set β) (set γ)
@[protected, instance]
def set.smul_comm_class {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ γ] [ γ] [ γ] :
(set β) (set γ)
@[protected, instance]
def set.is_scalar_tower {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ β] [ γ] [ γ] [ γ] :
(set γ)
@[protected, instance]
def set.is_scalar_tower' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ β] [ γ] [ γ] [ γ] :
(set β) (set γ)
@[protected, instance]
def set.is_scalar_tower'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ β] [ γ] [ γ] [ γ] :
(set β) (set γ)
@[protected, instance]
def set.is_central_scalar {α : Type u_1} {β : Type u_2} [ β] [ β] [ β] :
(set β)

### `set α` as a `(∪,*)`-semiring #

@[protected, instance]
def set.set_semiring.inhabited (α : Type u_1) :
def set.set_semiring (α : Type u_1) :
Type u_1

An alias for `set α`, which has a semiring structure given by `∪` as "addition" and pointwise multiplication `*` as "multiplication".

Equations
@[protected]
def set.up {α : Type u_1} (s : set α) :

The identitiy function `set α → set_semiring α`.

Equations
@[protected]
def set.set_semiring.down {α : Type u_1} (s : set.set_semiring α) :
set α

The identitiy function `set_semiring α → set α`.

Equations
@[protected, simp]
theorem set.down_up {α : Type u_1} {s : set α} :
s.up.down = s
@[protected, simp]
theorem set.up_down {α : Type u_1} {s : set.set_semiring α} :
s.down.up = s
@[protected, instance]
def set.set_semiring.add_comm_monoid {α : Type u_1} :
Equations
@[protected, instance]
def set.set_semiring.non_assoc_semiring {α : Type u_1}  :
Equations
@[protected, instance]
def set.set_semiring.non_unital_semiring {α : Type u_1} [semigroup α] :
Equations
@[protected, instance]
def set.set_semiring.semiring {α : Type u_1} [monoid α] :
Equations
@[protected, instance]
def set.set_semiring.comm_semiring {α : Type u_1} [comm_monoid α] :
Equations
@[protected, instance]
def set.add_action_set {α : Type u_1} {β : Type u_2} [add_monoid α] [ β] :
(set β)

An additive action of an additive monoid on a type β gives also an additive action on the subsets of β.

Equations
@[protected, instance]
def set.mul_action_set {α : Type u_1} {β : Type u_2} [monoid α] [ β] :
(set β)

A multiplicative action of a monoid on a type β gives also a multiplicative action on the subsets of β.

Equations
theorem set.image_add {α : Type u_1} {β : Type u_2} {s t : set α} [has_add α] [has_add β] (m : β) :
m '' (s + t) = m '' s + m '' t
theorem set.image_mul {α : Type u_1} {β : Type u_2} {s t : set α} [has_mul α] [has_mul β] (m : β) :
m '' s * t = (m '' s) * m '' t
theorem set.preimage_mul_preimage_subset {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] (m : β) {s t : set β} :
theorem set.preimage_add_preimage_subset {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (m : β) {s t : set β} :
def set.image_hom {α : Type u_1} {β : Type u_2} [monoid α] [monoid β] (f : α →* β) :

The image of a set under function is a ring homomorphism with respect to the pointwise operations on sets.

Equations
theorem zero_smul_set {α : Type u_1} {β : Type u_2} [has_zero α] [has_zero β] [ β] {s : set β} (h : s.nonempty) :
0 s = 0

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

theorem zero_smul_subset {α : Type u_1} {β : Type u_2} [has_zero α] [has_zero β] [ β] (s : set β) :
0 s 0
theorem subsingleton_zero_smul_set {α : Type u_1} {β : Type u_2} [has_zero α] [has_zero β] [ β] (s : set β) :
theorem smul_add_set {α : Type u_1} {β : Type u_2} [monoid α] [add_monoid β] [ β] (c : α) (s t : set β) :
c (s + t) = c s + c t
@[simp]
theorem smul_mem_smul_set_iff {α : Type u_1} {β : Type u_2} [group α] [ β] {A : set β} {a : α} {x : β} :
a x a A x A
@[simp]
theorem vadd_mem_vadd_set_iff {α : Type u_1} {β : Type u_2} [add_group α] [ β] {A : set β} {a : α} {x : β} :
a +ᵥ x a +ᵥ A x A
theorem mem_vadd_set_iff_neg_vadd_mem {α : Type u_1} {β : Type u_2} [add_group α] [ β] {A : set β} {a : α} {x : β} :
x a +ᵥ A -a +ᵥ x A
theorem mem_smul_set_iff_inv_smul_mem {α : Type u_1} {β : Type u_2} [group α] [ β] {A : set β} {a : α} {x : β} :
x a A a⁻¹ x A
theorem mem_neg_vadd_set_iff {α : Type u_1} {β : Type u_2} [add_group α] [ β] {A : set β} {a : α} {x : β} :
x -a +ᵥ A a +ᵥ x A
theorem mem_inv_smul_set_iff {α : Type u_1} {β : Type u_2} [group α] [ β] {A : set β} {a : α} {x : β} :
x a⁻¹ A a x A
theorem preimage_smul {α : Type u_1} {β : Type u_2} [group α] [ β] (a : α) (t : set β) :
(λ (x : β), a x) ⁻¹' t = a⁻¹ t
theorem preimage_vadd {α : Type u_1} {β : Type u_2} [add_group α] [ β] (a : α) (t : set β) :
(λ (x : β), a +ᵥ x) ⁻¹' t = -a +ᵥ t
theorem preimage_smul_inv {α : Type u_1} {β : Type u_2} [group α] [ β] (a : α) (t : set β) :
(λ (x : β), a⁻¹ x) ⁻¹' t = a t
theorem preimage_vadd_neg {α : Type u_1} {β : Type u_2} [add_group α] [ β] (a : α) (t : set β) :
(λ (x : β), -a +ᵥ x) ⁻¹' t = a +ᵥ t
@[simp]
theorem set_smul_subset_set_smul_iff {α : Type u_1} {β : Type u_2} [group α] [ β] {A B : set β} {a : α} :
a A a B A B
@[simp]
theorem set_vadd_subset_set_vadd_iff {α : Type u_1} {β : Type u_2} [add_group α] [ β] {A B : set β} {a : α} :
a +ᵥ A a +ᵥ B A B
theorem set_vadd_subset_iff {α : Type u_1} {β : Type u_2} [add_group α] [ β] {A B : set β} {a : α} :
a +ᵥ A B A -a +ᵥ B
theorem set_smul_subset_iff {α : Type u_1} {β : Type u_2} [group α] [ β] {A B : set β} {a : α} :
a A B A a⁻¹ B
theorem subset_set_smul_iff {α : Type u_1} {β : Type u_2} [group α] [ β] {A B : set β} {a : α} :
A a B a⁻¹ A B
theorem subset_set_vadd_iff {α : Type u_1} {β : Type u_2} [add_group α] [ β] {A B : set β} {a : α} :
A a +ᵥ B -a +ᵥ A B
@[simp]
theorem smul_mem_smul_set_iff₀ {α : Type u_1} {β : Type u_2} [ β] {a : α} (ha : a 0) (A : set β) (x : β) :
a x a A x A
theorem mem_smul_set_iff_inv_smul_mem₀ {α : Type u_1} {β : Type u_2} [ β] {a : α} (ha : a 0) (A : set β) (x : β) :
x a A a⁻¹ x A
theorem mem_inv_smul_set_iff₀ {α : Type u_1} {β : Type u_2} [ β] {a : α} (ha : a 0) (A : set β) (x : β) :
x a⁻¹ A a x A
theorem preimage_smul₀ {α : Type u_1} {β : Type u_2} [ β] {a : α} (ha : a 0) (t : set β) :
(λ (x : β), a x) ⁻¹' t = a⁻¹ t
theorem preimage_smul_inv₀ {α : Type u_1} {β : Type u_2} [ β] {a : α} (ha : a 0) (t : set β) :
(λ (x : β), a⁻¹ x) ⁻¹' t = a t
@[simp]
theorem set_smul_subset_set_smul_iff₀ {α : Type u_1} {β : Type u_2} [ β] {a : α} (ha : a 0) {A B : set β} :
a A a B A B
theorem set_smul_subset_iff₀ {α : Type u_1} {β : Type u_2} [ β] {a : α} (ha : a 0) {A B : set β} :
a A B A a⁻¹ B
theorem subset_set_smul_iff₀ {α : Type u_1} {β : Type u_2} [ β] {a : α} (ha : a 0) {A B : set β} :
A a B a⁻¹ A B
@[protected, instance]
def finset.has_one {α : Type u_1} [has_one α] :

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

Equations
@[protected, instance]
def finset.has_zero {α : Type u_1} [has_zero α] :

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

Equations
@[simp]
theorem finset.mem_one {α : Type u_1} {a : α} [has_one α] :
a 1 a = 1
@[simp]
theorem finset.mem_zero {α : Type u_1} {a : α} [has_zero α] :
a 0 a = 0
@[simp]
theorem finset.zero_subset {α : Type u_1} {s : finset α} [has_zero α] :
0 s 0 s
@[simp]
theorem finset.one_subset {α : Type u_1} {s : finset α} [has_one α] :
1 s 1 s
@[protected, instance]

The pointwise sum of two finite sets `s` and `t`: `s + t = { x + y | x ∈ s, y ∈ t }`.

Equations
@[protected, instance]
def finset.has_mul {α : Type u_1} [decidable_eq α] [has_mul α] :

The pointwise product of two finite sets `s` and `t`: `st = s ⬝ t = s * t = { x * y | x ∈ s, y ∈ t }`.

Equations
theorem finset.add_def {α : Type u_1} {s t : finset α} [decidable_eq α] [has_add α] :
s + t = finset.image (λ (p : α × α), p.fst + p.snd) (s.product t)
theorem finset.mul_def {α : Type u_1} {s t : finset α} [decidable_eq α] [has_mul α] :
s * t = finset.image (λ (p : α × α), (p.fst) * p.snd) (s.product t)
theorem finset.mem_mul {α : Type u_1} {s t : finset α} [decidable_eq α] [has_mul α] {x : α} :
x s * t ∃ (y z : α), y s z t y * z = x
theorem finset.mem_add {α : Type u_1} {s t : finset α} [decidable_eq α] [has_add α] {x : α} :
x s + t ∃ (y z : α), y s z t y + z = x
@[simp, norm_cast]
theorem finset.coe_add {α : Type u_1} {s t : finset α} [decidable_eq α] [has_add α] :
(s + t) = s + t
@[simp, norm_cast]
theorem finset.coe_mul {α : Type u_1} {s t : finset α} [decidable_eq α] [has_mul α] :
s * t = (s) * t
theorem finset.mul_mem_mul {α : Type u_1} {s t : finset α} [decidable_eq α] [has_mul α] {x y : α} (hx : x s) (hy : y t) :
x * y s * t
theorem finset.add_mem_add {α : Type u_1} {s t : finset α} [decidable_eq α] [has_add α] {x y : α} (hx : x s) (hy : y t) :
x + y s + t
theorem finset.add_card_le {α : Type u_1} {s t : finset α} [decidable_eq α] [has_add α] :
(s + t).card (s.card) * t.card
theorem finset.mul_card_le {α : Type u_1} {s t : finset α} [decidable_eq α] [has_mul α] :
(s * t).card (s.card) * t.card
@[simp]
theorem finset.empty_mul {α : Type u_1} [decidable_eq α] [has_mul α] (s : finset α) :
@[simp]
theorem finset.empty_add {α : Type u_1} [decidable_eq α] [has_add α] (s : finset α) :
@[simp]
theorem finset.add_empty {α : Type u_1} [decidable_eq α] [has_add α] (s : finset α) :
@[simp]
theorem finset.mul_empty {α : Type u_1} [decidable_eq α] [has_mul α] (s : finset α) :
@[simp]
theorem finset.add_nonempty_iff {α : Type u_1} [decidable_eq α] [has_add α] (s t : finset α) :
(s + t).nonempty
@[simp]
theorem finset.mul_nonempty_iff {α : Type u_1} [decidable_eq α] [has_mul α] (s t : finset α) :
(s * t).nonempty
theorem finset.add_subset_add {α : Type u_1} {s₁ s₂ t₁ t₂ : finset α} [decidable_eq α] [has_add α] (hs : s₁ s₂) (ht : t₁ t₂) :
s₁ + t₁ s₂ + t₂
theorem finset.mul_subset_mul {α : Type u_1} {s₁ s₂ t₁ t₂ : finset α} [decidable_eq α] [has_mul α] (hs : s₁ s₂) (ht : t₁ t₂) :
s₁ * t₁ s₂ * t₂
@[simp]
theorem finset.mul_singleton {α : Type u_1} {s : finset α} [decidable_eq α] [has_mul α] (a : α) :
s * {a} = finset.image (λ (_x : α), _x * a) s
@[simp]
theorem finset.add_singleton {α : Type u_1} {s : finset α} [decidable_eq α] [has_add α] (a : α) :
s + {a} = finset.image (λ (_x : α), _x + a) s
@[simp]
theorem finset.singleton_add {α : Type u_1} {s : finset α} [decidable_eq α] [has_add α] (a : α) :
{a} + s = s
@[simp]
theorem finset.singleton_mul {α : Type u_1} {s : finset α} [decidable_eq α] [has_mul α] (a : α) :
{a} * s = s
@[simp]
theorem finset.singleton_add_singleton {α : Type u_1} [decidable_eq α] [has_add α] (a b : α) :
{a} + {b} = {a + b}
@[simp]
theorem finset.singleton_mul_singleton {α : Type u_1} [decidable_eq α] [has_mul α] (a b : α) :
{a} * {b} = {a * b}
theorem finset.mul_zero_subset {α : Type u_1} [decidable_eq α] (s : finset α) :
s * 0 0
theorem finset.zero_mul_subset {α : Type u_1} [decidable_eq α] (s : finset α) :
0 * s 0
theorem finset.nonempty.mul_zero {α : Type u_1} {s : finset α} [decidable_eq α] (hs : s.nonempty) :
s * 0 = 0
theorem finset.nonempty.zero_mul {α : Type u_1} {s : finset α} [decidable_eq α] (hs : s.nonempty) :
0 * s = 0
theorem finset.singleton_zero_mul {α : Type u_1} [decidable_eq α] (s : finset α) :
{0} * s {0}
theorem finset.singleton_one {α : Type u_1} [has_one α] :
{1} = 1
theorem finset.singleton_zero {α : Type u_1} [has_zero α] :
{0} = 0
theorem finset.one_mem_one {α : Type u_1} [has_one α] :
1 1
theorem finset.zero_mem_zero {α : Type u_1} [has_zero α] :
0 0
theorem finset.one_nonempty {α : Type u_1} [has_one α] :
theorem finset.zero_nonempty {α : Type u_1} [has_zero α] :
@[simp]
theorem finset.image_zero {α : Type u_1} {β : Type u_2} [decidable_eq β] [has_zero α] {f : α → β} :
0 = {f 0}
@[simp]
theorem finset.image_one {α : Type u_1} {β : Type u_2} [decidable_eq β] [has_one α] {f : α → β} :
1 = {f 1}
theorem finset.add_image_prod {α : Type u_1} {s t : finset α} [decidable_eq α] [has_add α] :
finset.image (λ (x : α × α), x.fst + x.snd) (s.product t) = s + t
theorem finset.image_mul_prod {α : Type u_1} {s t : finset α} [decidable_eq α] [has_mul α] :
finset.image (λ (x : α × α), (x.fst) * x.snd) (s.product t) = s * t
@[simp]
theorem finset.image_mul_left {α : Type u_1} {a : α} {t : finset α} [decidable_eq α] [group α] :
finset.image (λ (b : α), a * b) t = t.preimage (λ (b : α), a⁻¹ * b) _
@[simp]
theorem finset.image_add_left {α : Type u_1} {a : α} {t : finset α} [decidable_eq α] [add_group α] :
finset.image (λ (b : α), a + b) t = t.preimage (λ (b : α), -a + b) _
@[simp]
theorem finset.image_mul_right {α : Type u_1} {t : finset α} {b : α} [decidable_eq α] [group α] :
finset.image (λ (a : α), a * b) t = t.preimage (λ (a : α), a * b⁻¹) _
@[simp]
theorem finset.image_add_right {α : Type u_1} {t : finset α} {b : α} [decidable_eq α] [add_group α] :
finset.image (λ (a : α), a + b) t = t.preimage (λ (a : α), a + -b) _
theorem finset.image_add_left' {α : Type u_1} {a : α} {t : finset α} [decidable_eq α] [add_group α] :
finset.image (λ (b : α), -a + b) t = t.preimage (λ (b : α), a + b) _
theorem finset.image_mul_left' {α : Type u_1} {a : α} {t : finset α} [decidable_eq α] [group α] :
finset.image (λ (b : α), a⁻¹ * b) t = t.preimage (λ (b : α), a * b) _
theorem finset.image_add_right' {α : Type u_1} {t : finset α} {b : α} [decidable_eq α] [add_group α] :
finset.image (λ (a : α), a + -b) t = t.preimage (λ (a : α), a + b) _
theorem finset.image_mul_right' {α : Type u_1} {t : finset α} {b : α} [decidable_eq α] [group α] :
finset.image (λ (a : α), a * b⁻¹) t = t.preimage (λ (a : α), a * b) _
@[simp]
theorem finset.preimage_mul_left_singleton {α : Type u_1} {a b : α} [group α] :
{b}.preimage (has_mul.mul a) _ = {a⁻¹ * b}
@[simp]
theorem finset.preimage_add_left_singleton {α : Type u_1} {a b : α} [add_group α] :
@[simp]
theorem finset.preimage_mul_right_singleton {α : Type u_1} {a b : α} [group α] :
{b}.preimage (λ (_x : α), _x * a) _ = {b * a⁻¹}
@[simp]
theorem finset.preimage_add_right_singleton {α : Type u_1} {a b : α} [add_group α] :
{b}.preimage (λ (_x : α), _x + a) _ = {b + -a}
@[simp]
theorem finset.preimage_mul_left_one {α : Type u_1} {a : α} [group α] :
1.preimage (λ (b : α), a * b) _ = {a⁻¹}
@[simp]
theorem finset.preimage_add_left_zero {α : Type u_1} {a : α} [add_group α] :
0.preimage (λ (b : α), a + b) _ = {-a}
@[simp]
theorem finset.preimage_add_right_zero {α : Type u_1} {b : α} [add_group α] :
0.preimage (λ (a : α), a + b) _ = {-b}
@[simp]
theorem finset.preimage_mul_right_one {α : Type u_1} {b : α} [group α] :
1.preimage (λ (a : α), a * b) _ = {b⁻¹}
theorem finset.preimage_add_left_zero' {α : Type u_1} {a : α} [add_group α] :
0.preimage (λ (b : α), -a + b) _ = {a}
theorem finset.preimage_mul_left_one' {α : Type u_1} {a : α} [group α] :
1.preimage (λ (b : α), a⁻¹ * b) _ = {a}
theorem finset.preimage_mul_right_one' {α : Type u_1} {b : α} [group α] :
1.preimage (λ (a : α), a * b⁻¹) _ = {b}
theorem finset.preimage_add_right_zero' {α : Type u_1} {b : α} [add_group α] :
0.preimage (λ (a : α), a + -b) _ = {b}
@[protected]
theorem finset.add_comm {α : Type u_1} {s t : finset α} [decidable_eq α]  :
s + t = t + s
@[protected]
theorem finset.mul_comm {α : Type u_1} {s t : finset α} [decidable_eq α]  :
s * t = t * s
@[protected, instance]
def finset.add_zero_class {α : Type u_1} [decidable_eq α]  :

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

Equations
@[protected, instance]
def finset.mul_one_class {α : Type u_1} [decidable_eq α]  :

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

Equations
@[protected, instance]
def finset.semigroup {α : Type u_1} [decidable_eq α] [semigroup α] :

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

Equations
@[protected, instance]
def finset.add_semigroup {α : Type u_1} [decidable_eq α]  :

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

Equations
@[protected, instance]
def finset.monoid {α : Type u_1} [decidable_eq α] [monoid α] :

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

Equations
@[protected, instance]

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

Equations
@[protected, instance]
def finset.comm_monoid {α : Type u_1} [decidable_eq α] [comm_monoid α] :

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

Equations
@[protected, instance]
def finset.add_comm_monoid {α : Type u_1} [decidable_eq α]  :

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

Equations
theorem finset.subset_mul {M : Type u_1} [monoid M] {S S' : set M} {U : finset M} (f : U S * S') :
∃ (T T' : finset M), T S T' S' U T * T'

A finite set `U` contained in the product of two sets `S * S'` is also contained in the product of two finite sets `T * T' ⊆ S * S'`.

theorem finset.subset_add {M : Type u_1} [add_monoid M] {S S' : set M} {U : finset M} (f : U S + S') :
∃ (T T' : finset M), T S T' S' U T + T'

Some lemmas about pointwise multiplication and submonoids. Ideally we put these in `group_theory.submonoid.basic`, but currently we cannot because that file is imported by this.

theorem submonoid.mul_subset {M : Type u_6} [monoid M] {s t : set M} {S : submonoid M} (hs : s S) (ht : t S) :
s * t S
theorem add_submonoid.add_subset {M : Type u_6} [add_monoid M] {s t : set M} {S : add_submonoid M} (hs : s S) (ht : t S) :
s + t S
theorem add_submonoid.add_subset_closure {M : Type u_6} [add_monoid M] {s t u : set M} (hs : s u) (ht : t u) :
s + t
theorem submonoid.mul_subset_closure {M : Type u_6} [monoid M] {s t u : set M} (hs : s u) (ht : t u) :
s * t