Pointwise actions of finsets #
Instances #
instance
Finset.smulCommClass_finset
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[DecidableEq γ]
[SMul α γ]
[SMul β γ]
[SMulCommClass α β γ]
:
SMulCommClass α β (Finset γ)
instance
Finset.vaddCommClass_finset
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[DecidableEq γ]
[VAdd α γ]
[VAdd β γ]
[VAddCommClass α β γ]
:
VAddCommClass α β (Finset γ)
instance
Finset.smulCommClass_finset'
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[DecidableEq γ]
[SMul α γ]
[SMul β γ]
[SMulCommClass α β γ]
:
SMulCommClass α (Finset β) (Finset γ)
instance
Finset.vaddCommClass_finset'
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[DecidableEq γ]
[VAdd α γ]
[VAdd β γ]
[VAddCommClass α β γ]
:
VAddCommClass α (Finset β) (Finset γ)
instance
Finset.smulCommClass_finset''
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[DecidableEq γ]
[SMul α γ]
[SMul β γ]
[SMulCommClass α β γ]
:
SMulCommClass (Finset α) β (Finset γ)
instance
Finset.vaddCommClass_finset''
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[DecidableEq γ]
[VAdd α γ]
[VAdd β γ]
[VAddCommClass α β γ]
:
VAddCommClass (Finset α) β (Finset γ)
instance
Finset.smulCommClass
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[DecidableEq γ]
[SMul α γ]
[SMul β γ]
[SMulCommClass α β γ]
:
SMulCommClass (Finset α) (Finset β) (Finset γ)
instance
Finset.vaddCommClass
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[DecidableEq γ]
[VAdd α γ]
[VAdd β γ]
[VAddCommClass α β γ]
:
VAddCommClass (Finset α) (Finset β) (Finset γ)
instance
Finset.isScalarTower
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[DecidableEq γ]
[SMul α β]
[SMul α γ]
[SMul β γ]
[IsScalarTower α β γ]
:
IsScalarTower α β (Finset γ)
instance
Finset.vaddAssocClass
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[DecidableEq γ]
[VAdd α β]
[VAdd α γ]
[VAdd β γ]
[VAddAssocClass α β γ]
:
VAddAssocClass α β (Finset γ)
instance
Finset.isScalarTower'
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[DecidableEq γ]
[DecidableEq β]
[SMul α β]
[SMul α γ]
[SMul β γ]
[IsScalarTower α β γ]
:
IsScalarTower α (Finset β) (Finset γ)
instance
Finset.vaddAssocClass'
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[DecidableEq γ]
[DecidableEq β]
[VAdd α β]
[VAdd α γ]
[VAdd β γ]
[VAddAssocClass α β γ]
:
VAddAssocClass α (Finset β) (Finset γ)
instance
Finset.isScalarTower''
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[DecidableEq γ]
[DecidableEq β]
[SMul α β]
[SMul α γ]
[SMul β γ]
[IsScalarTower α β γ]
:
IsScalarTower (Finset α) (Finset β) (Finset γ)
instance
Finset.vaddAssocClass''
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[DecidableEq γ]
[DecidableEq β]
[VAdd α β]
[VAdd α γ]
[VAdd β γ]
[VAddAssocClass α β γ]
:
VAddAssocClass (Finset α) (Finset β) (Finset γ)
instance
Finset.isCentralScalar
{α : Type u_2}
{β : Type u_3}
[DecidableEq β]
[SMul α β]
[SMul αᵐᵒᵖ β]
[IsCentralScalar α β]
:
IsCentralScalar α (Finset β)
instance
Finset.isCentralVAdd
{α : Type u_2}
{β : Type u_3}
[DecidableEq β]
[VAdd α β]
[VAdd αᵃᵒᵖ β]
[IsCentralVAdd α β]
:
IsCentralVAdd α (Finset β)
theorem
Finset.mul_singleton
{α : Type u_2}
[Mul α]
[DecidableEq α]
{s : Finset α}
(a : α)
:
s * {a} = MulOpposite.op a • s
theorem
Finset.add_singleton
{α : Type u_2}
[Add α]
[DecidableEq α]
{s : Finset α}
(a : α)
:
s + {a} = AddOpposite.op a +ᵥ s
theorem
Finset.singleton_mul
{α : Type u_2}
[Mul α]
[DecidableEq α]
{s : Finset α}
(a : α)
:
{a} * s = a • s
theorem
Finset.singleton_add
{α : Type u_2}
[Add α]
[DecidableEq α]
{s : Finset α}
(a : α)
:
{a} + s = a +ᵥ s
theorem
Finset.smul_finset_subset_mul
{α : Type u_2}
[Mul α]
[DecidableEq α]
{s t : Finset α}
{a : α}
:
a ∈ s → a • t ⊆ s * t
theorem
Finset.vadd_finset_subset_add
{α : Type u_2}
[Add α]
[DecidableEq α]
{s t : Finset α}
{a : α}
:
a ∈ s → a +ᵥ t ⊆ s + t
theorem
Finset.op_smul_finset_subset_mul
{α : Type u_2}
[Mul α]
[DecidableEq α]
{s t : Finset α}
{a : α}
:
a ∈ t → MulOpposite.op a • s ⊆ s * t
theorem
Finset.op_vadd_finset_subset_add
{α : Type u_2}
[Add α]
[DecidableEq α]
{s t : Finset α}
{a : α}
:
a ∈ t → AddOpposite.op a +ᵥ s ⊆ s + t
@[simp]
theorem
Finset.biUnion_op_smul_finset
{α : Type u_2}
[Mul α]
[DecidableEq α]
(s t : Finset α)
:
(t.biUnion fun (a : α) => MulOpposite.op a • s) = s * t
@[simp]
theorem
Finset.biUnion_op_vadd_finset
{α : Type u_2}
[Add α]
[DecidableEq α]
(s t : Finset α)
:
(t.biUnion fun (a : α) => AddOpposite.op a +ᵥ s) = s + t
theorem
Finset.mul_subset_iff_left
{α : Type u_2}
[Mul α]
[DecidableEq α]
{s t u : Finset α}
:
s * t ⊆ u ↔ ∀ a ∈ s, a • t ⊆ u
theorem
Finset.add_subset_iff_left
{α : Type u_2}
[Add α]
[DecidableEq α]
{s t u : Finset α}
:
s + t ⊆ u ↔ ∀ a ∈ s, a +ᵥ t ⊆ u
theorem
Finset.mul_subset_iff_right
{α : Type u_2}
[Mul α]
[DecidableEq α]
{s t u : Finset α}
:
s * t ⊆ u ↔ ∀ b ∈ t, MulOpposite.op b • s ⊆ u
theorem
Finset.add_subset_iff_right
{α : Type u_2}
[Add α]
[DecidableEq α]
{s t u : Finset α}
:
s + t ⊆ u ↔ ∀ b ∈ t, AddOpposite.op b +ᵥ s ⊆ u
theorem
Finset.op_smul_finset_mul_eq_mul_smul_finset
{α : Type u_2}
[Semigroup α]
[DecidableEq α]
(a : α)
(s t : Finset α)
:
MulOpposite.op a • s * t = s * a • t
theorem
Finset.op_vadd_finset_add_eq_add_vadd_finset
{α : Type u_2}
[AddSemigroup α]
[DecidableEq α]
(a : α)
(s t : Finset α)
:
(AddOpposite.op a +ᵥ s) + t = s + (a +ᵥ t)
theorem
Finset.pairwiseDisjoint_smul_iff
{α : Type u_2}
[Mul α]
[IsLeftCancelMul α]
[DecidableEq α]
{s : Set α}
{t : Finset α}
:
(s.PairwiseDisjoint fun (x : α) => x • t) ↔ Set.InjOn (fun (p : α × α) => p.1 * p.2) (s ×ˢ ↑t)
theorem
Finset.pairwiseDisjoint_vadd_iff
{α : Type u_2}
[Add α]
[IsLeftCancelAdd α]
[DecidableEq α]
{s : Set α}
{t : Finset α}
:
(s.PairwiseDisjoint fun (x : α) => x +ᵥ t) ↔ Set.InjOn (fun (p : α × α) => p.1 + p.2) (s ×ˢ ↑t)
theorem
Finset.image_smul_distrib
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[DecidableEq β]
[Mul α]
[Mul β]
[FunLike F α β]
[MulHomClass F α β]
(f : F)
(a : α)
(s : Finset α)
:
@[simp]
@[simp]
@[simp]
theorem
Finset.mul_mem_smul_finset_iff
{α : Type u_2}
[Group α]
[DecidableEq α]
(a : α)
{b : α}
{s : Finset α}
:
a * b ∈ a • s ↔ b ∈ s
@[simp]
theorem
Finset.add_mem_vadd_finset_iff
{α : Type u_2}
[AddGroup α]
[DecidableEq α]
(a : α)
{b : α}
{s : Finset α}
:
a + b ∈ a +ᵥ s ↔ b ∈ s
@[simp]
@[simp]
@[simp]
@[simp]
theorem
Finset.card_dvd_card_smul_right
{α : Type u_2}
{β : Type u_3}
[DecidableEq β]
[Group α]
[MulAction α β]
{t : Finset β}
{s : Finset α}
:
((fun (x : α) => x • t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s • t).card
If the left cosets of t by elements of s are disjoint (but not necessarily distinct!), then
the size of t divides the size of s • t.
theorem
Finset.card_dvd_card_mul_left
{α : Type u_2}
[Group α]
[DecidableEq α]
{s t : Finset α}
:
((fun (b : α) => image (fun (a : α) => a * b) s) '' ↑t).PairwiseDisjoint id → s.card ∣ (s * t).card
If the right cosets of s by elements of t are disjoint (but not necessarily distinct!), then
the size of s divides the size of s * t.
theorem
Finset.card_dvd_card_add_left
{α : Type u_2}
[AddGroup α]
[DecidableEq α]
{s t : Finset α}
:
((fun (b : α) => image (fun (a : α) => a + b) s) '' ↑t).PairwiseDisjoint id → s.card ∣ (s + t).card
If the right cosets of s by elements of t are disjoint (but not necessarily
distinct!), then the size of s divides the size of s + t.
theorem
Finset.card_dvd_card_mul_right
{α : Type u_2}
[Group α]
[DecidableEq α]
{s t : Finset α}
:
((fun (x : α) => x • t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s * t).card
If the left cosets of t by elements of s are disjoint (but not necessarily distinct!), then
the size of t divides the size of s * t.
theorem
Finset.card_dvd_card_add_right
{α : Type u_2}
[AddGroup α]
[DecidableEq α]
{s t : Finset α}
:
((fun (x : α) => x +ᵥ t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s + t).card
If the left cosets of t by elements of s are disjoint (but not necessarily
distinct!), then the size of t divides the size of s + t.
@[simp]
theorem
Finset.inv_smul_finset_distrib
{α : Type u_2}
[Group α]
[DecidableEq α]
(a : α)
(s : Finset α)
:
(a • s)⁻¹ = MulOpposite.op a⁻¹ • s⁻¹
@[simp]
theorem
Finset.neg_vadd_finset_distrib
{α : Type u_2}
[AddGroup α]
[DecidableEq α]
(a : α)
(s : Finset α)
:
@[simp]
theorem
Finset.inv_op_smul_finset_distrib
{α : Type u_2}
[Group α]
[DecidableEq α]
(a : α)
(s : Finset α)
:
(MulOpposite.op a • s)⁻¹ = a⁻¹ • s⁻¹
@[simp]
theorem
Finset.neg_op_vadd_finset_distrib
{α : Type u_2}
[AddGroup α]
[DecidableEq α]
(a : α)
(s : Finset α)
:
@[implicit_reducible]
instance
Nat.decidablePred_mem_vadd_set
{s : Set ℕ}
[DecidablePred fun (x : ℕ) => x ∈ s]
(a : ℕ)
:
DecidablePred fun (x : ℕ) => x ∈ a +ᵥ s