Mathlib.Algebra.Ring.Action.Pointwise.Set

Module docstring

{"# 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 "}

Set.smul_set_neg theorem

: a • -t = -(a • t)

Full source

@[simp]
lemma smul_set_neg : a • -t = -(a • t) := by
  simp_rw [← image_smul, ← image_neg_eq_neg, image_image, smul_neg]

Scalar Multiplication Commutes with Set Negation: $a \cdot (-t) = -(a \cdot t)$

Informal description

For any scalar $a$ in a monoid $M$ and any subset $t$ of an additive group $A$, the scalar multiplication satisfies $a \cdot (-t) = -(a \cdot t)$, where $-t$ denotes the negation of each element in $t$ and $a \cdot t$ denotes the scalar multiplication of $a$ with each element in $t$.

Set.smul_neg theorem

: s • -t = -(s • t)

Full source

@[simp]
protected lemma smul_neg : s • -t = -(s • t) := by
  simp_rw [← image_neg_eq_neg]
  exact image_image2_right_comm smul_neg

Pointwise Scalar Multiplication Commutes with Set Negation: $s \cdot (-t) = -(s \cdot t)$

Informal description

For any subset $s$ of a monoid $M$ and any subset $t$ of an additive group $A$, the pointwise scalar multiplication satisfies $s \cdot (-t) = -(s \cdot t)$, where $-t$ denotes the negation of each element in $t$ and $s \cdot t$ denotes the set $\{x \cdot y \mid x \in s, y \in t\}$.

Set.add_smul_subset theorem

(a b : α) (s : Set β) : (a + b) • s ⊆ a • s + b • s

Full source

lemma add_smul_subset (a b : α) (s : Set β) : (a + b) • s ⊆ a • s + b • s := by
  rintro _ ⟨x, hx, rfl⟩
  simpa only [add_smul] using add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hx)

Subset Property: $(a + b) \cdot s \subseteq a \cdot s + b \cdot s$

Informal description

For any elements $a, b$ in a semiring $\alpha$ and any subset $s$ of an $\alpha$-module $\beta$, the set $(a + b) \cdot s$ is a subset of the Minkowski sum $a \cdot s + b \cdot s$, where $\cdot$ denotes scalar multiplication of a set.

Set.neg_smul_set theorem

: -a • t = -(a • t)

Full source

@[simp]
lemma neg_smul_set : -a • t = -(a • t) := by
  simp_rw [← image_smul, ← image_neg_eq_neg, image_image, neg_smul]

Negative Scalar Multiplication on Sets: $-a \cdot t = -(a \cdot t)$

Informal description

For any scalar $a$ in a ring and any subset $t$ of a module over that ring, the scalar multiplication satisfies $-a \cdot t = -(a \cdot t)$, where $-a \cdot t$ denotes the set $\{-a \cdot x \mid x \in t\}$ and $-(a \cdot t)$ denotes the set $\{-y \mid y \in a \cdot t\}$.

Set.neg_smul theorem

: -s • t = -(s • t)

Full source

@[simp]
protected lemma neg_smul : -s • t = -(s • t) := by
  simp_rw [← image_neg_eq_neg]
  exact image2_image_left_comm neg_smul

Negative Scalar Multiplication on Sets: $-s \cdot t = -(s \cdot t)$

Informal description

For any subset $s$ of a ring $\alpha$ and any subset $t$ of an $\alpha$-module $\beta$, the pointwise scalar multiplication satisfies $-s \cdot t = -(s \cdot t)$, where $-s \cdot t$ denotes the set $\{-x \cdot y \mid x \in s, y \in t\}$ and $-(s \cdot t)$ denotes the set $\{-z \mid z \in s \cdot t\}$.