Pointwise operations of finsets in a group with zero #
This file proves properties of pointwise operations of finsets in a group with zero.
@[implicit_reducible]
def
Finset.smulZeroClass
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[Zero β]
[SMulZeroClass α β]
:
SMulZeroClass α (Finset β)
If scalar multiplication by elements of α sends (0 : β) to zero,
then the same is true for (0 : Finset β).
Instances For
@[implicit_reducible]
noncomputable def
Finset.distribSMul
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[AddZeroClass β]
[DistribSMul α β]
:
DistribSMul α (Finset β)
If the scalar multiplication (· • ·) : α → β → β is distributive,
then so is (· • ·) : α → Finset β → Finset β.
Instances For
@[implicit_reducible]
noncomputable def
Finset.distribMulAction
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[Monoid α]
[AddMonoid β]
[DistribMulAction α β]
:
DistribMulAction α (Finset β)
A distributive multiplicative action of a monoid on an additive monoid β gives a distributive
multiplicative action on Finset β.
Instances For
@[implicit_reducible]
noncomputable def
Finset.mulDistribMulAction
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[Monoid α]
[Monoid β]
[MulDistribMulAction α β]
:
MulDistribMulAction α (Finset β)
A multiplicative action of a monoid on a monoid β gives a multiplicative action on Set β.
Instances For
instance
Finset.instNoZeroDivisors
{α : Type u_1}
[DecidableEq α]
[Zero α]
[Mul α]
[NoZeroDivisors α]
:
NoZeroDivisors (Finset α)
theorem
Finset.smul_zero_subset
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[Zero β]
[SMulZeroClass α β]
(s : Finset α)
:
s • 0 ⊆ 0
theorem
Finset.Nonempty.smul_zero
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[Zero β]
[SMulZeroClass α β]
{s : Finset α}
(hs : s.Nonempty)
:
s • 0 = 0
theorem
Finset.zero_mem_smul_finset
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[Zero β]
[SMulZeroClass α β]
{t : Finset β}
{a : α}
(h : 0 ∈ t)
:
0 ∈ a • t
Note that we have neither SMulWithZero α (Finset β) nor SMulWithZero (Finset α) (Finset β)
because 0 • ∅ ≠ 0.
theorem
Finset.zero_smul_subset
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[Zero α]
[Zero β]
[SMulWithZero α β]
(t : Finset β)
:
0 • t ⊆ 0
theorem
Finset.Nonempty.zero_smul
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[Zero α]
[Zero β]
[SMulWithZero α β]
{t : Finset β}
(ht : t.Nonempty)
:
0 • t = 0
@[simp]
theorem
Finset.zero_smul_finset
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[Zero α]
[Zero β]
[SMulWithZero α β]
{s : Finset β}
(h : s.Nonempty)
:
0 • s = 0
A nonempty set is scaled by zero to the singleton set containing zero.
theorem
Finset.zero_smul_finset_subset
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[Zero α]
[Zero β]
[SMulWithZero α β]
(s : Finset β)
:
0 • s ⊆ 0
@[simp]
theorem
Finset.smul_mem_smul_finset_iff₀
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[GroupWithZero α]
[MulAction α β]
{s : Finset β}
{a : α}
{b : β}
(ha : a ≠ 0)
:
a • b ∈ a • s ↔ b ∈ s
theorem
Finset.inv_smul_mem_iff₀
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[GroupWithZero α]
[MulAction α β]
{s : Finset β}
{a : α}
{b : β}
(ha : a ≠ 0)
:
a⁻¹ • b ∈ s ↔ b ∈ a • s
theorem
Finset.mem_inv_smul_finset_iff₀
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[GroupWithZero α]
[MulAction α β]
{s : Finset β}
{a : α}
{b : β}
(ha : a ≠ 0)
:
b ∈ a⁻¹ • s ↔ a • b ∈ s
@[simp]
theorem
Finset.smul_finset_subset_smul_finset_iff₀
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[GroupWithZero α]
[MulAction α β]
{s t : Finset β}
{a : α}
(ha : a ≠ 0)
:
a • s ⊆ a • t ↔ s ⊆ t
theorem
Finset.smul_finset_subset_iff₀
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[GroupWithZero α]
[MulAction α β]
{s t : Finset β}
{a : α}
(ha : a ≠ 0)
:
a • s ⊆ t ↔ s ⊆ a⁻¹ • t
theorem
Finset.subset_smul_finset_iff₀
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[GroupWithZero α]
[MulAction α β]
{s t : Finset β}
{a : α}
(ha : a ≠ 0)
:
s ⊆ a • t ↔ a⁻¹ • s ⊆ t
theorem
Finset.smul_finset_inter₀
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[GroupWithZero α]
[MulAction α β]
{s t : Finset β}
{a : α}
(ha : a ≠ 0)
:
a • (s ∩ t) = a • s ∩ a • t
theorem
Finset.smul_finset_sdiff₀
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[GroupWithZero α]
[MulAction α β]
{s t : Finset β}
{a : α}
(ha : a ≠ 0)
:
theorem
Finset.smul_finset_symmDiff₀
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[GroupWithZero α]
[MulAction α β]
{s t : Finset β}
{a : α}
(ha : a ≠ 0)
:
theorem
Finset.smul_finset_univ₀
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[GroupWithZero α]
[MulAction α β]
{a : α}
[Fintype β]
(ha : a ≠ 0)
:
theorem
Finset.smul_univ₀
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[GroupWithZero α]
[MulAction α β]
[Fintype β]
{s : Finset α}
(hs : ¬s ⊆ 0)
:
theorem
Finset.smul_univ₀'
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[GroupWithZero α]
[MulAction α β]
[Fintype β]
{s : Finset α}
(hs : s.Nontrivial)
:
@[simp]
theorem
Finset.inv_smul_finset_distrib₀
{α : Type u_1}
[GroupWithZero α]
[DecidableEq α]
(a : α)
(s : Finset α)
:
(a • s)⁻¹ = MulOpposite.op a⁻¹ • s⁻¹
theorem
Finset.inv_op_smul_finset_distrib₀
{α : Type u_1}
[GroupWithZero α]
[DecidableEq α]
(a : α)
(s : Finset α)
:
(MulOpposite.op a • s)⁻¹ = a⁻¹ • s⁻¹
@[simp]
theorem
Finset.smul_finset_neg
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[Monoid α]
[AddGroup β]
[DistribMulAction α β]
(a : α)
(t : Finset β)
:
@[simp]
theorem
Finset.smul_neg
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
[Monoid α]
[AddGroup β]
[DistribMulAction α β]
(s : Finset α)
(t : Finset β)
: