Pointwise operations of finsets in a group with zero

This file proves properties of pointwise operations of finsets in a group with zero.

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 β).

Equations

• Finset.smulZeroClass = Function.Injective.smulZeroClass { toFun := Finset.toSet, map_zero' := ⋯ } ⋯ ⋯

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 β.

Equations

• Finset.distribSMul = Function.Injective.distribSMul Finset.coeAddMonoidHom ⋯ ⋯

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 β.

Equations

• Finset.distribMulAction = Function.Injective.distribMulAction Finset.coeAddMonoidHom ⋯ ⋯

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 β.

Equations

• Finset.mulDistribMulAction = Function.Injective.mulDistribMulAction Finset.coeMonoidHom ⋯ ⋯

instance Finset.instNoZeroDivisors {α : Type u_1} [DecidableEq α] [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors (Finset α)

Equations

• ⋯ = ⋯

instance Finset.noZeroSMulDivisors {α : Type u_1} {β : Type u_2} [DecidableEq β] [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors (Finset α) (Finset β)

Equations

• ⋯ = ⋯

instance Finset.noZeroSMulDivisors_finset {α : Type u_1} {β : Type u_2} [DecidableEq β] [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors α (Finset β)

Equations

• ⋯ = ⋯

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

theorem Finset.zero_mem_smul_finset_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] [Zero β] [SMulZeroClass α β] {t : Finset β} {a : α} [Zero α] [NoZeroSMulDivisors α β] (ha : a ≠ 0) : 0 ∈ a • t ↔ 0 ∈ 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

theorem Finset.zero_mem_smul_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] [Zero α] [Zero β] [SMulWithZero α β] {s : Finset α} {t : Finset β} [NoZeroSMulDivisors α β] : 0 ∈ s • t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Note that Finset is not a MulZeroClass because 0 * ∅ ≠ 0.

theorem Finset.mul_zero_subset {α : Type u_1} [DecidableEq α] [MulZeroClass α] (s : Finset α) : s * 0 ⊆ 0

theorem Finset.zero_mul_subset {α : Type u_1} [DecidableEq α] [MulZeroClass α] (s : Finset α) : 0 * s ⊆ 0

theorem Finset.Nonempty.mul_zero {α : Type u_1} [DecidableEq α] [MulZeroClass α] {s : Finset α} (hs : s.Nonempty) : s * 0 = 0

theorem Finset.Nonempty.zero_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] {s : Finset α} (hs : s.Nonempty) : 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 : Finset β} {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 : Finset β} {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 : Finset β} {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 : Finset β} {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 : Finset β} {t : Finset β} {a : α} (ha : a ≠ 0) : a • (s \ t) = a • s \ a • t

theorem Finset.smul_finset_symmDiff₀ {α : Type u_1} {β : Type u_2} [DecidableEq β] [GroupWithZero α] [MulAction α β] {s : Finset β} {t : Finset β} {a : α} (ha : a ≠ 0) : a • symmDiff s t = symmDiff (a • s) (a • t)

theorem Finset.smul_finset_univ₀ {α : Type u_1} {β : Type u_2} [DecidableEq β] [GroupWithZero α] [MulAction α β] {a : α} [Fintype β] (ha : a ≠ 0) : a • Finset.univ = Finset.univ

theorem Finset.smul_univ₀ {α : Type u_1} {β : Type u_2} [DecidableEq β] [GroupWithZero α] [MulAction α β] [Fintype β] {s : Finset α} (hs : ¬s ⊆ 0) : s • Finset.univ = Finset.univ

theorem Finset.smul_univ₀' {α : Type u_1} {β : Type u_2} [DecidableEq β] [GroupWithZero α] [MulAction α β] [Fintype β] {s : Finset α} (hs : s.Nontrivial) : s • Finset.univ = Finset.univ

theorem Finset.div_zero_subset {α : Type u_1} [GroupWithZero α] [DecidableEq α] (s : Finset α) : s / 0 ⊆ 0

theorem Finset.zero_div_subset {α : Type u_1} [GroupWithZero α] [DecidableEq α] (s : Finset α) : 0 / s ⊆ 0

theorem Finset.Nonempty.div_zero {α : Type u_1} [GroupWithZero α] [DecidableEq α] {s : Finset α} (hs : s.Nonempty) : s / 0 = 0

theorem Finset.Nonempty.zero_div {α : Type u_1} [GroupWithZero α] [DecidableEq α] {s : Finset α} (hs : s.Nonempty) : 0 / s = 0

@[simp]

theorem Finset.inv_zero {α : Type u_1} [GroupWithZero α] [DecidableEq α] : 0⁻¹ = 0

@[simp]

theorem Finset.inv_smul_finset_distrib₀ {α : Type u_1} [GroupWithZero α] [DecidableEq α] (a : α) (s : Finset α) : (a • s)⁻¹ = MulOpposite.op a⁻¹ • s⁻¹

@[simp]

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 β) : a • -t = -(a • t)

@[simp]

theorem Finset.smul_neg {α : Type u_1} {β : Type u_2} [DecidableEq β] [Monoid α] [AddGroup β] [DistribMulAction α β] (s : Finset α) (t : Finset β) : s • -t = -(s • t)