Pointwise actions of finsets #

Instances #

instance Finset.smulCommClass_finset {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :

SMulCommClass α β (Finset γ)

source

instance Finset.vaddCommClass_finset {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :

VAddCommClass α β (Finset γ)

source

instance Finset.smulCommClass_finset' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :

SMulCommClass α (Finset β) (Finset γ)

source

instance Finset.vaddCommClass_finset' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :

VAddCommClass α (Finset β) (Finset γ)

source

instance Finset.smulCommClass_finset'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :

SMulCommClass (Finset α) β (Finset γ)

source

instance Finset.vaddCommClass_finset'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :

VAddCommClass (Finset α) β (Finset γ)

source

instance Finset.smulCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :

SMulCommClass (Finset α) (Finset β) (Finset γ)

source

instance Finset.vaddCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :

VAddCommClass (Finset α) (Finset β) (Finset γ)

source

instance Finset.isScalarTower {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :

IsScalarTower α β (Finset γ)

source

instance Finset.vaddAssocClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :

VAddAssocClass α β (Finset γ)

source

instance Finset.isScalarTower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [DecidableEq β] [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :

IsScalarTower α (Finset β) (Finset γ)

source

instance Finset.vaddAssocClass' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [DecidableEq β] [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :

VAddAssocClass α (Finset β) (Finset γ)

source

instance Finset.isScalarTower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [DecidableEq β] [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :

IsScalarTower (Finset α) (Finset β) (Finset γ)

source

instance Finset.vaddAssocClass'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq γ] [DecidableEq β] [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :

VAddAssocClass (Finset α) (Finset β) (Finset γ)

source

instance Finset.isCentralScalar {α : Type u_2} {β : Type u_3} [DecidableEq β] [SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α β] :

IsCentralScalar α (Finset β)

source

instance Finset.isCentralVAdd {α : Type u_2} {β : Type u_3} [DecidableEq β] [VAdd α β] [VAdd αᵃᵒᵖ β] [IsCentralVAdd α β] :

IsCentralVAdd α (Finset β)

source

def Finset.mulAction {α : Type u_2} {β : Type u_3} [DecidableEq β] [DecidableEq α] [Monoid α] [MulAction α β] :

MulAction (Finset α) (Finset β)

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

Equations

Finset.mulAction = { toSMul := Finset.smul, one_smul := ⋯, mul_smul := ⋯ }

Instances For

source

def Finset.addAction {α : Type u_2} {β : Type u_3} [DecidableEq β] [DecidableEq α] [AddMonoid α] [AddAction α β] :

AddAction (Finset α) (Finset β)

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

Equations

Finset.addAction = { toVAdd := Finset.vadd, zero_vadd := ⋯, add_vadd := ⋯ }

Instances For

source

def Finset.mulActionFinset {α : Type u_2} {β : Type u_3} [DecidableEq β] [Monoid α] [MulAction α β] :

MulAction α (Finset β)

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

Equations

Finset.mulActionFinset = Function.Injective.mulAction Finset.toSet ⋯ ⋯

Instances For

source

def Finset.addActionFinset {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddMonoid α] [AddAction α β] :

AddAction α (Finset β)

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

Equations

Finset.addActionFinset = Function.Injective.addAction Finset.toSet ⋯ ⋯

Instances For

source

theorem Finset.mul_singleton {α : Type u_2} [Mul α] [DecidableEq α] {s : Finset α} (a : α) :

s * {a} = MulOpposite.op a • s

source

theorem Finset.add_singleton {α : Type u_2} [Add α] [DecidableEq α] {s : Finset α} (a : α) :

s + {a} = AddOpposite.op a +ᵥ s

source

theorem Finset.singleton_mul {α : Type u_2} [Mul α] [DecidableEq α] {s : Finset α} (a : α) :

{a} * s = a • s

source

theorem Finset.singleton_add {α : Type u_2} [Add α] [DecidableEq α] {s : Finset α} (a : α) :

{a} + s = a +ᵥ s

source

theorem Finset.smul_finset_subset_mul {α : Type u_2} [Mul α] [DecidableEq α] {s t : Finset α} {a : α} :

a ∈ s → a • t ⊆ s * t

source

theorem Finset.vadd_finset_subset_add {α : Type u_2} [Add α] [DecidableEq α] {s t : Finset α} {a : α} :

a ∈ s → a +ᵥ t ⊆ s + t

source

theorem Finset.op_smul_finset_subset_mul {α : Type u_2} [Mul α] [DecidableEq α] {s t : Finset α} {a : α} :

a ∈ t → MulOpposite.op a • s ⊆ s * t

source

theorem Finset.op_vadd_finset_subset_add {α : Type u_2} [Add α] [DecidableEq α] {s t : Finset α} {a : α} :

a ∈ t → AddOpposite.op a +ᵥ s ⊆ s + t

source

@[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

source

@[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

source

theorem Finset.mul_subset_iff_left {α : Type u_2} [Mul α] [DecidableEq α] {s t u : Finset α} :

s * t ⊆ u ↔ ∀ a ∈ s, a • t ⊆ u

source

theorem Finset.add_subset_iff_left {α : Type u_2} [Add α] [DecidableEq α] {s t u : Finset α} :

s + t ⊆ u ↔ ∀ a ∈ s, a +ᵥ t ⊆ u

source

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

source

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

source

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

source

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)

source

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)

source

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)

source

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

image (⇑f) (a • s) = f a • image (⇑f) s

source

theorem Finset.image_vadd_distrib {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) (a : α) (s : Finset α) :

image (⇑f) (a +ᵥ s) = f a +ᵥ image (⇑f) s

source

@[simp]

theorem Finset.smul_mem_smul_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {b : β} (a : α) :

a • b ∈ a • s ↔ b ∈ s

source

@[simp]

theorem Finset.vadd_mem_vadd_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {b : β} (a : α) :

a +ᵥ b ∈ a +ᵥ s ↔ b ∈ s

source

@[simp]

theorem Finset.mul_mem_smul_finset_iff {α : Type u_2} [Group α] [DecidableEq α] (a : α) {b : α} {s : Finset α} :

a * b ∈ a • s ↔ b ∈ s

source

@[simp]

theorem Finset.add_mem_vadd_finset_iff {α : Type u_2} [AddGroup α] [DecidableEq α] (a : α) {b : α} {s : Finset α} :

a + b ∈ a +ᵥ s ↔ b ∈ s

source

theorem Finset.inv_smul_mem_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {a : α} {b : β} :

a⁻¹ • b ∈ s ↔ b ∈ a • s

source

theorem Finset.neg_vadd_mem_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {a : α} {b : β} :

-a +ᵥ b ∈ s ↔ b ∈ a +ᵥ s

source

theorem Finset.mem_inv_smul_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s : Finset β} {a : α} {b : β} :

b ∈ a⁻¹ • s ↔ a • b ∈ s

source

theorem Finset.mem_neg_vadd_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s : Finset β} {a : α} {b : β} :

b ∈ -a +ᵥ s ↔ a +ᵥ b ∈ s

source

@[simp]

theorem Finset.smul_finset_subset_smul_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s t : Finset β} {a : α} :

a • s ⊆ a • t ↔ s ⊆ t

source

@[simp]

theorem Finset.vadd_finset_subset_vadd_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s t : Finset β} {a : α} :

a +ᵥ s ⊆ a +ᵥ t ↔ s ⊆ t

source

theorem Finset.smul_finset_subset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s t : Finset β} {a : α} :

a • s ⊆ t ↔ s ⊆ a⁻¹ • t

source

theorem Finset.vadd_finset_subset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s t : Finset β} {a : α} :

a +ᵥ s ⊆ t ↔ s ⊆ -a +ᵥ t

source

theorem Finset.subset_smul_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s t : Finset β} {a : α} :

s ⊆ a • t ↔ a⁻¹ • s ⊆ t

source

theorem Finset.subset_vadd_finset_iff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s t : Finset β} {a : α} :

s ⊆ a +ᵥ t ↔ -a +ᵥ s ⊆ t

source

theorem Finset.smul_finset_inter {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s t : Finset β} {a : α} :

a • (s ∩ t) = a • s ∩ a • t

source

theorem Finset.vadd_finset_inter {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s t : Finset β} {a : α} :

a +ᵥ s ∩ t = (a +ᵥ s) ∩ (a +ᵥ t)

source

theorem Finset.smul_finset_sdiff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s t : Finset β} {a : α} :

a • (s \ t) = a • s \ a • t

source

theorem Finset.vadd_finset_sdiff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s t : Finset β} {a : α} :

a +ᵥ s \ t = (a +ᵥ s) \ (a +ᵥ t)

source

theorem Finset.smul_finset_symmDiff {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {s t : Finset β} {a : α} :

a • symmDiff s t = symmDiff (a • s) (a • t)

source

theorem Finset.vadd_finset_symmDiff {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {s t : Finset β} {a : α} :

a +ᵥ symmDiff s t = symmDiff (a +ᵥ s) (a +ᵥ t)

source

@[simp]

theorem Finset.smul_finset_univ {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] {a : α} [Fintype β] :

a • univ = univ

source

@[simp]

theorem Finset.vadd_finset_univ {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {a : α} [Fintype β] :

a +ᵥ univ = univ

source

@[simp]

theorem Finset.smul_univ {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] [Fintype β] {s : Finset α} (hs : s.Nonempty) :

s • univ = univ

source

@[simp]

theorem Finset.vadd_univ {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] [Fintype β] {s : Finset α} (hs : s.Nonempty) :

s +ᵥ univ = univ

source

@[simp]

theorem Finset.card_smul_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [Group α] [MulAction α β] (a : α) (s : Finset β) :

(a • s).card = s.card

source

@[simp]

theorem Finset.card_vadd_finset {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] (a : α) (s : Finset β) :

(a +ᵥ s).card = s.card

source

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.

source

theorem Finset.card_dvd_card_vadd_right {α : Type u_2} {β : Type u_3} [DecidableEq β] [AddGroup α] [AddAction α β] {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.

source

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.

source

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.

source

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.

source

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.

source

@[simp]

theorem Finset.inv_smul_finset_distrib {α : Type u_2} [Group α] [DecidableEq α] (a : α) (s : Finset α) :

(a • s)⁻¹ = MulOpposite.op a⁻¹ • s⁻¹

source

@[simp]

theorem Finset.neg_vadd_finset_distrib {α : Type u_2} [AddGroup α] [DecidableEq α] (a : α) (s : Finset α) :

-(a +ᵥ s) = AddOpposite.op (-a) +ᵥ -s

source

@[simp]

theorem Finset.inv_op_smul_finset_distrib {α : Type u_2} [Group α] [DecidableEq α] (a : α) (s : Finset α) :

(MulOpposite.op a • s)⁻¹ = a⁻¹ • s⁻¹

source

@[simp]

theorem Finset.neg_op_vadd_finset_distrib {α : Type u_2} [AddGroup α] [DecidableEq α] (a : α) (s : Finset α) :

-(AddOpposite.op a +ᵥ s) = -a +ᵥ -s

source

theorem Fintype.piFinset_smul {ι : Type u_5} {α : ι → Type u_6} {β : ι → Type u_7} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → SMul (α i) (β i)] (s : (i : ι) → Finset (α i)) (t : (i : ι) → Finset (β i)) :

(piFinset fun (i : ι) => s i • t i) = piFinset s • piFinset t

source

theorem Fintype.piFinset_vadd {ι : Type u_5} {α : ι → Type u_6} {β : ι → Type u_7} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → VAdd (α i) (β i)] (s : (i : ι) → Finset (α i)) (t : (i : ι) → Finset (β i)) :

(piFinset fun (i : ι) => s i +ᵥ t i) = piFinset s +ᵥ piFinset t

source

theorem Fintype.piFinset_smul_finset {ι : Type u_5} {α : ι → Type u_6} {β : ι → Type u_7} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → SMul (α i) (β i)] (a : (i : ι) → α i) (s : (i : ι) → Finset (β i)) :

(piFinset fun (i : ι) => a i • s i) = a • piFinset s

source

theorem Fintype.piFinset_vadd_finset {ι : Type u_5} {α : ι → Type u_6} {β : ι → Type u_7} [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → VAdd (α i) (β i)] (a : (i : ι) → α i) (s : (i : ι) → Finset (β i)) :

(piFinset fun (i : ι) => a i +ᵥ s i) = a +ᵥ piFinset s

source

instance Nat.decidablePred_mem_vadd_set {s : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ s] (a : ℕ) :

DecidablePred fun (x : ℕ) => x ∈ a +ᵥ s

Equations

a.decidablePred_mem_vadd_set n = decidable_of_iff' (a ≤ n ∧ n - a ∈ s) ⋯

Documentation

Mathlib.Algebra.Group.Action.Pointwise.Finset

Pointwise actions of finsets #

Instances #