Pointwise operations of sets in a ring #
This file proves properties of pointwise operations of sets in a ring.
Tags #
set multiplication, set addition, pointwise addition, pointwise multiplication, pointwise subtraction
@[simp]
theorem
Set.smul_set_neg
{α : Type u_1}
{β : Type u_2}
[Monoid α]
[AddGroup β]
[DistribMulAction α β]
(a : α)
(t : Set β)
:
@[simp]
theorem
Set.smul_neg
{α : Type u_1}
{β : Type u_2}
[Monoid α]
[AddGroup β]
[DistribMulAction α β]
(s : Set α)
(t : Set β)
:
theorem
Set.add_smul_subset
{α : Type u_1}
{β : Type u_2}
[Semiring α]
[AddCommMonoid β]
[Module α β]
(a b : α)
(s : Set β)
:
(a + b) • s ⊆ a • s + b • s
theorem
Set.zero_mem_smul_set_iff
{α : Type u_1}
{β : Type u_2}
[Semiring α]
[AddCommMonoid β]
[Module α β]
[IsDomain α]
[Module.IsTorsionFree α β]
{a : α}
{t : Set β}
(ha : a ≠ 0)
:
0 ∈ a • t ↔ 0 ∈ t
theorem
Set.zero_mem_smul_iff
{α : Type u_1}
{β : Type u_2}
[Semiring α]
[AddCommMonoid β]
[Module α β]
[IsDomain α]
[Module.IsTorsionFree α β]
{s : Set α}
{t : Set β}
:
@[simp]
theorem
Set.neg_smul_set
{α : Type u_1}
{β : Type u_2}
[Ring α]
[AddCommGroup β]
[Module α β]
(a : α)
(t : Set β)
:
@[simp]
theorem
Set.neg_smul
{α : Type u_1}
{β : Type u_2}
[Ring α]
[AddCommGroup β]
[Module α β]
(s : Set α)
(t : Set β)
: