Pointwise addition, multiplication, and scalar multiplication of sets. #
This file defines pointwise algebraic operations on sets.
- For a type
αwith multiplication, multiplication is defined onset αby takings * tto be the set of allx * ywherex ∈ sandy ∈ t. Similarly for addition. - For
αa semigroup,set αis a semigroup. - If
αis a (commutative) monoid, we define an aliasset_semiring αforset α, 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 ofset βbyset αand a separate scalar multiplication ofset β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 ofsimp).
Tags #
set multiplication, set addition, pointwise addition, pointwise multiplication
Properties about 1 #
@[protected, instance]
The set (1 : set α) is defined as {1} in locale pointwise.
Equations
- set.has_one = {one := {1}}
@[protected, instance]
The set (0 : set α) is defined as {0} in locale pointwise.
Equations
- set.has_zero = {zero := {0}}
@[simp]
@[simp]
Properties about multiplication #
@[protected, instance]
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 α] :
set.image2 has_mul.mul s t = s * t
@[simp]
theorem
set.image2_add
{α : Type u_1}
{s t : set α}
[has_add α] :
set.image2 has_add.add s t = s + t
@[simp]
theorem
set.preimage_mul_left_singleton
{α : Type u_1}
{a b : α}
[group α] :
has_mul.mul a ⁻¹' {b} = {a⁻¹ * b}
@[simp]
theorem
set.preimage_add_left_singleton
{α : Type u_1}
{a b : α}
[add_group α] :
has_add.add a ⁻¹' {b} = {-a + b}
@[protected]
@[protected]
@[protected, instance]
set α is an add_zero_class under pointwise operations if α is.
Equations
- set.add_zero_class = {zero := 0, add := has_add.add set.has_add, zero_add := _, add_zero := _}
@[protected, instance]
set α is a mul_one_class under pointwise operations if α is.
Equations
- set.mul_one_class = {one := 1, mul := has_mul.mul set.has_mul, one_mul := _, mul_one := _}
@[protected, instance]
set α is an add_semigroup under pointwise operations if α is.
Equations
- set.add_semigroup = {add := has_add.add set.has_add, add_assoc := _}
@[protected, instance]
set α is a semigroup under pointwise operations if α is.
Equations
- set.semigroup = {mul := has_mul.mul set.has_mul, mul_assoc := _}
@[protected, instance]
set α is a monoid under pointwise operations if α is.
Equations
- set.monoid = {mul := semigroup.mul set.semigroup, mul_assoc := _, one := mul_one_class.one set.mul_one_class, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (set α)), npow_zero' := _, npow_succ' := _}
@[protected, instance]
set α is an add_monoid under pointwise operations if α is.
Equations
- set.add_monoid = {add := add_semigroup.add set.add_semigroup, add_assoc := _, zero := add_zero_class.zero set.add_zero_class, zero_add := _, add_zero := _, nsmul := nsmul_rec (add_zero_class.to_has_add (set α)), nsmul_zero' := _, nsmul_succ' := _}
@[protected, instance]
set α is a comm_monoid under pointwise operations if α is.
Equations
- set.comm_monoid = {mul := monoid.mul set.monoid, mul_assoc := _, one := monoid.one set.monoid, one_mul := _, mul_one := _, npow := monoid.npow set.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, instance]
set α is an add_comm_monoid under pointwise operations if α is.
Equations
- set.add_comm_monoid = {add := add_monoid.add set.add_monoid, add_assoc := _, zero := add_monoid.zero set.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul set.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
theorem
set.nsmul_mem_nsmul
{α : Type u_1}
{s : set α}
{a : α}
[add_monoid α]
(ha : a ∈ s)
(n : ℕ) :
@[simp]
theorem
set.singleton_add_hom_apply
{α : Type u_1}
[has_add α]
(ᾰ : α) :
⇑set.singleton_add_hom ᾰ = {ᾰ}
@[simp]
theorem
set.singleton_mul_hom_apply
{α : Type u_1}
[has_mul α]
(ᾰ : α) :
⇑set.singleton_mul_hom ᾰ = {ᾰ}
@[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
- set.decidable_mem_mul = λ (_x : α), decidable_of_iff (∃ (x y : α), x ∈ s ∧ y ∈ t ∧ x * y = _x) _
@[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
- set.decidable_mem_pow n = 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 : α), set.decidable_mem_mul a)) n
@[simp]
singleton is a monoid hom.
Equations
- set.singleton_hom = {to_fun := singleton set.has_singleton, map_one' := _, map_mul' := _}
def
set.fintype_add
{α : Type u_1}
[has_add α]
[decidable_eq α]
(s t : set α)
[hs : fintype ↥s]
[ht : fintype ↥t] :
addition preserves finiteness
Equations
- s.fintype_add t = set.fintype_image2 (λ (a b : α), a + b) s t
def
set.fintype_mul
{α : Type u_1}
[has_mul α]
[decidable_eq α]
(s t : set α)
[hs : fintype ↥s]
[ht : fintype ↥t] :
multiplication preserves finiteness
Equations
- s.fintype_mul t = set.fintype_image2 (λ (a b : α), a * b) s t
theorem
set.mem_finset_sum
{α : Type u_1}
{ι : Type u_4}
[add_comm_monoid α]
(t : finset ι)
(f : ι → set α)
(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 : α) :
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 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}
[add_comm_monoid α]
[fintype ι]
(f : ι → set α)
(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 ∈ t → g 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}
[add_comm_monoid α]
(t : finset ι)
(f : ι → set α)
(g : ι → α)
(hg : ∀ (i : ι), i ∈ t → g 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 ∈ t → f₁ 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}
[add_comm_monoid α]
(t : finset ι)
(f₁ f₂ : ι → set α)
(hf : ∀ {i : ι}, i ∈ t → f₁ 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}
[add_comm_monoid M]
(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.
Properties about inversion #
@[protected, instance]
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]
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]
@[simp]
@[simp]
Properties about scalar multiplication #
@[protected, instance]
The translation of a set (x +ᵥ s : set β) by a scalar x ∶ α is
defined as {x +ᵥ y | y ∈ s} in locale pointwise.
Equations
- set.has_vadd_set = {vadd := λ (a : α), set.image (has_vadd.vadd a)}
@[protected, instance]
The scaling of a set (x • s : set β) by a scalar x ∶ α is defined as {x • y | y ∈ s}
in locale pointwise.
Equations
- set.has_scalar_set = {smul := λ (a : α), set.image (has_scalar.smul a)}
@[simp]
theorem
set.smul_mem_smul_set
{α : Type u_1}
{β : Type u_2}
{a : α}
{y : β}
[has_scalar α β]
{t : set β}
(hy : y ∈ t) :
theorem
set.smul_set_inter₀
{α : Type u_1}
{β : Type u_2}
{a : α}
[group_with_zero α]
[mul_action α β]
{s t : set β}
(ha : a ≠ 0) :
theorem
set.smul_set_inter_subset
{α : Type u_1}
{β : Type u_2}
{a : α}
[has_scalar α β]
{s t : set β} :
@[simp]
theorem
set.smul_set_mono
{α : Type u_1}
{β : Type u_2}
{a : α}
[has_scalar α β]
{s t : set β}
(h : s ⊆ t) :
@[simp]
theorem
set.image2_smul
{α : Type u_1}
{β : Type u_2}
{s : set α}
[has_scalar α β]
{t : set β} :
set.image2 has_scalar.smul s t = s • t
@[simp]
theorem
set.image2_vadd
{α : Type u_1}
{β : Type u_2}
{s : set α}
[has_vadd α β]
{t : set β} :
set.image2 has_vadd.vadd s t = s +ᵥ t
theorem
set.mem_smul_of_mem
{α : Type u_1}
{β : Type u_2}
{s : set α}
[has_scalar α β]
{t : set β}
{a : α}
{b : β}
(ha : a ∈ s)
(hb : b ∈ t) :
@[simp]
@[simp]
@[protected, instance]
def
set.vadd_comm_class_set
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_vadd α γ]
[has_vadd β γ]
[vadd_comm_class α β γ] :
vadd_comm_class α (set β) (set γ)
@[protected, instance]
def
set.smul_comm_class_set
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_scalar α γ]
[has_scalar β γ]
[smul_comm_class α β γ] :
smul_comm_class α (set β) (set γ)
@[protected, instance]
def
set.vadd_comm_class_set'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_vadd α γ]
[has_vadd β γ]
[vadd_comm_class α β γ] :
vadd_comm_class (set α) β (set γ)
@[protected, instance]
def
set.smul_comm_class_set'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_scalar α γ]
[has_scalar β γ]
[smul_comm_class α β γ] :
smul_comm_class (set α) β (set γ)
@[protected, instance]
def
set.vadd_comm_class
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_vadd α γ]
[has_vadd β γ]
[vadd_comm_class α β γ] :
vadd_comm_class (set α) (set β) (set γ)
@[protected, instance]
def
set.smul_comm_class
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_scalar α γ]
[has_scalar β γ]
[smul_comm_class α β γ] :
smul_comm_class (set α) (set β) (set γ)
@[protected, instance]
def
set.is_scalar_tower
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_scalar α β]
[has_scalar α γ]
[has_scalar β γ]
[is_scalar_tower α β γ] :
is_scalar_tower α β (set γ)
@[protected, instance]
def
set.is_scalar_tower'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_scalar α β]
[has_scalar α γ]
[has_scalar β γ]
[is_scalar_tower α β γ] :
is_scalar_tower α (set β) (set γ)
@[protected, instance]
def
set.is_scalar_tower''
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_scalar α β]
[has_scalar α γ]
[has_scalar β γ]
[is_scalar_tower α β γ] :
is_scalar_tower (set α) (set β) (set γ)
@[protected, instance]
def
set.is_central_scalar
{α : Type u_1}
{β : Type u_2}
[has_scalar α β]
[has_scalar αᵐᵒᵖ β]
[is_central_scalar α β] :
is_central_scalar α (set β)
@[protected, instance]
An alias for set α, which has a semiring structure given by ∪ as "addition" and pointwise
multiplication * as "multiplication".
Equations
- set.set_semiring α = set α
@[protected]
The identitiy function set_semiring α → set α.
@[protected, simp]
@[protected, instance]
Equations
- set.set_semiring.add_comm_monoid = {add := λ (s t : set.set_semiring α), s ∪ t, add_assoc := _, zero := ∅, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul._default ∅ (λ (s t : set.set_semiring α), s ∪ t) set.empty_union set.union_empty, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[protected, instance]
Equations
- set.set_semiring.non_unital_non_assoc_semiring = {add := add_comm_monoid.add set.set_semiring.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero set.set_semiring.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul set.set_semiring.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul set.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}
@[protected, instance]
Equations
- set.set_semiring.non_assoc_semiring = {add := non_unital_non_assoc_semiring.add set.set_semiring.non_unital_non_assoc_semiring, add_assoc := _, zero := non_unital_non_assoc_semiring.zero set.set_semiring.non_unital_non_assoc_semiring, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul set.set_semiring.non_unital_non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_non_assoc_semiring.mul set.set_semiring.non_unital_non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := mul_one_class.one set.mul_one_class, one_mul := _, mul_one := _}
@[protected, instance]
Equations
- set.set_semiring.non_unital_semiring = {add := non_unital_non_assoc_semiring.add set.set_semiring.non_unital_non_assoc_semiring, add_assoc := _, zero := non_unital_non_assoc_semiring.zero set.set_semiring.non_unital_non_assoc_semiring, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul set.set_semiring.non_unital_non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_non_assoc_semiring.mul set.set_semiring.non_unital_non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}
@[protected, instance]
Equations
- set.set_semiring.semiring = {add := non_assoc_semiring.add set.set_semiring.non_assoc_semiring, add_assoc := _, zero := non_assoc_semiring.zero set.set_semiring.non_assoc_semiring, zero_add := _, add_zero := _, nsmul := non_assoc_semiring.nsmul set.set_semiring.non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_assoc_semiring.mul set.set_semiring.non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := non_assoc_semiring.one set.set_semiring.non_assoc_semiring, one_mul := _, mul_one := _, npow := monoid_with_zero.npow._default non_assoc_semiring.one non_assoc_semiring.mul set.set_semiring.semiring._proof_14 set.set_semiring.semiring._proof_15, npow_zero' := _, npow_succ' := _}
@[protected, instance]
Equations
- set.set_semiring.comm_semiring = {add := semiring.add set.set_semiring.semiring, add_assoc := _, zero := semiring.zero set.set_semiring.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul set.set_semiring.semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := comm_monoid.mul set.comm_monoid, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := comm_monoid.one set.comm_monoid, one_mul := _, mul_one := _, npow := comm_monoid.npow set.comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, instance]
def
set.add_action_set
{α : Type u_1}
{β : Type u_2}
[add_monoid α]
[add_action α β] :
add_action α (set β)
An additive action of an additive monoid on a type β gives also an additive action on the subsets of β.
Equations
- set.add_action_set = {to_has_vadd := {vadd := has_vadd.vadd set.has_vadd_set}, zero_vadd := _, add_vadd := _}
@[protected, instance]
def
set.mul_action_set
{α : Type u_1}
{β : Type u_2}
[monoid α]
[mul_action α β] :
mul_action α (set β)
A multiplicative action of a monoid on a type β gives also a multiplicative action on the subsets of β.
Equations
- set.mul_action_set = {to_has_scalar := {smul := has_scalar.smul set.has_scalar_set}, one_smul := _, mul_smul := _}
The image of a set under function is a ring homomorphism with respect to the pointwise operations on sets.
theorem
zero_smul_set
{α : Type u_1}
{β : Type u_2}
[has_zero α]
[has_zero β]
[smul_with_zero α β]
{s : set β}
(h : s.nonempty) :
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 β]
[smul_with_zero α β]
(s : set β) :
theorem
subsingleton_zero_smul_set
{α : Type u_1}
{β : Type u_2}
[has_zero α]
[has_zero β]
[smul_with_zero α β]
(s : set β) :
(0 • s).subsingleton
theorem
smul_add_set
{α : Type u_1}
{β : Type u_2}
[monoid α]
[add_monoid β]
[distrib_mul_action α β]
(c : α)
(s t : set β) :
@[simp]
theorem
smul_mem_smul_set_iff
{α : Type u_1}
{β : Type u_2}
[group α]
[mul_action α β]
{A : set β}
{a : α}
{x : β} :
@[simp]
theorem
vadd_mem_vadd_set_iff
{α : Type u_1}
{β : Type u_2}
[add_group α]
[add_action α β]
{A : set β}
{a : α}
{x : β} :
theorem
preimage_smul
{α : Type u_1}
{β : Type u_2}
[group α]
[mul_action α β]
(a : α)
(t : set β) :
theorem
preimage_vadd
{α : Type u_1}
{β : Type u_2}
[add_group α]
[add_action α β]
(a : α)
(t : set β) :
theorem
preimage_smul_inv
{α : Type u_1}
{β : Type u_2}
[group α]
[mul_action α β]
(a : α)
(t : set β) :
theorem
preimage_vadd_neg
{α : Type u_1}
{β : Type u_2}
[add_group α]
[add_action α β]
(a : α)
(t : set β) :
@[simp]
theorem
set_smul_subset_set_smul_iff
{α : Type u_1}
{β : Type u_2}
[group α]
[mul_action α β]
{A B : set β}
{a : α} :
@[simp]
theorem
set_vadd_subset_set_vadd_iff
{α : Type u_1}
{β : Type u_2}
[add_group α]
[add_action α β]
{A B : set β}
{a : α} :
@[simp]
theorem
smul_mem_smul_set_iff₀
{α : Type u_1}
{β : Type u_2}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
(A : set β)
(x : β) :
theorem
mem_smul_set_iff_inv_smul_mem₀
{α : Type u_1}
{β : Type u_2}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
(A : set β)
(x : β) :
theorem
mem_inv_smul_set_iff₀
{α : Type u_1}
{β : Type u_2}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
(A : set β)
(x : β) :
theorem
preimage_smul₀
{α : Type u_1}
{β : Type u_2}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
(t : set β) :
theorem
preimage_smul_inv₀
{α : Type u_1}
{β : Type u_2}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
(t : set β) :
@[simp]
theorem
set_smul_subset_set_smul_iff₀
{α : Type u_1}
{β : Type u_2}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
{A B : set β} :
theorem
set_smul_subset_iff₀
{α : Type u_1}
{β : Type u_2}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
{A B : set β} :
theorem
subset_set_smul_iff₀
{α : Type u_1}
{β : Type u_2}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
{A B : set β} :
@[protected, instance]
The finset (1 : finset α) is defined as {1} in locale pointwise.
Equations
- finset.has_one = {one := {1}}
@[protected, instance]
The finset (0 : finset α) is defined as {0} in locale pointwise.
Equations
- finset.has_zero = {zero := {0}}
@[protected, instance]
The pointwise sum of two finite sets s and t:
s + t = { x + y | x ∈ s, y ∈ t }.
@[protected, instance]
The pointwise product of two finite sets s and t:
st = s ⬝ t = s * t = { x * y | x ∈ s, y ∈ t }.
theorem
finset.mul_mem_mul
{α : Type u_1}
{s t : finset α}
[decidable_eq α]
[has_mul α]
{x y : α}
(hx : x ∈ s)
(hy : y ∈ t) :
theorem
finset.add_mem_add
{α : Type u_1}
{s t : finset α}
[decidable_eq α]
[has_add α]
{x y : α}
(hx : x ∈ s)
(hy : y ∈ t) :
@[simp]
@[simp]
@[simp]
@[simp]
theorem
finset.add_subset_add
{α : Type u_1}
{s₁ s₂ t₁ t₂ : finset α}
[decidable_eq α]
[has_add α]
(hs : s₁ ⊆ s₂)
(ht : t₁ ⊆ t₂) :
theorem
finset.mul_subset_mul
{α : Type u_1}
{s₁ s₂ t₁ t₂ : finset α}
[decidable_eq α]
[has_mul α]
(hs : s₁ ⊆ s₂)
(ht : t₁ ⊆ 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 = finset.image (has_add.add a) s
@[simp]
theorem
finset.singleton_mul
{α : Type u_1}
{s : finset α}
[decidable_eq α]
[has_mul α]
(a : α) :
{a} * s = finset.image (has_mul.mul a) s
@[simp]
@[simp]
theorem
finset.nonempty.mul_zero
{α : Type u_1}
{s : finset α}
[decidable_eq α]
[mul_zero_class α]
(hs : s.nonempty) :
theorem
finset.nonempty.zero_mul
{α : Type u_1}
{s : finset α}
[decidable_eq α]
[mul_zero_class α]
(hs : s.nonempty) :
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
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) :
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 ⊆ ↑(add_submonoid.closure u)
theorem
submonoid.mul_subset_closure
{M : Type u_6}
[monoid M]
{s t u : set M}
(hs : s ⊆ u)
(ht : t ⊆ u) :
s * t ⊆ ↑(submonoid.closure u)
theorem
submonoid.closure_mul_le
{M : Type u_6}
[monoid M]
(S T : set M) :
submonoid.closure (S * T) ≤ submonoid.closure S ⊔ submonoid.closure T
theorem
submonoid.pow_smul_mem_closure_smul
{M : Type u_6}
[monoid M]
{N : Type u_1}
[comm_monoid N]
[mul_action M N]
[is_scalar_tower M N N]
(r : M)
(s : set N)
{x : N}
(hx : x ∈ submonoid.closure s) :
theorem
group.card_pow_eq_card_pow_card_univ
{G : Type u_6}
[group G]
[fintype G]
(S : set G)
[Π (k : ℕ), decidable_pred (λ (_x : G), _x ∈ S ^ k)]
(k : ℕ) :
fintype.card G ≤ k → fintype.card ↥(S ^ k) = fintype.card ↥(S ^ fintype.card G)
theorem
add_group.card_pow_eq_card_pow_card_univ
{G : Type u_6}
[add_group G]
[fintype G]
(S : set G)
[Π (k : ℕ), decidable_pred (λ (_x : G), _x ∈ k • S)]
(k : ℕ) :
fintype.card G ≤ k → fintype.card ↥(k • S) = fintype.card ↥(fintype.card G • S)