Mathlib.Algebra.Ring.Submonoid.Basic

MulMemClass.mul_right_mem_add_closure theorem

(ha : a ∈ closure (S : Set R)) (hb : b ∈ S) : a * b ∈ closure (S : Set R)

Full source

/-- The product of an element of the additive closure of a multiplicative subsemigroup `M`
and an element of `M` is contained in the additive closure of `M`. -/
lemma mul_right_mem_add_closure (ha : a ∈ closure (S : Set R)) (hb : b ∈ S) :
    a * b ∈ closure (S : Set R) := by
  induction ha using closure_induction with
  | mem r hr => exact AddSubmonoid.mem_closure.mpr fun y hy => hy (mul_mem hr hb)
  | one => simp only [zero_mul, zero_mem _]
  | mul r s _ _ hr hs => simpa only [add_mul] using add_mem hr hs

Right Multiplication Preserves Additive Closure of Multiplicative Subsemigroup

Informal description

Let $R$ be a non-unital non-associative semiring and $S$ a multiplicative subsemigroup of $R$. For any element $a$ in the additive closure of $S$ and any element $b \in S$, the product $a \cdot b$ is contained in the additive closure of $S$.

MulMemClass.mul_mem_add_closure theorem

(ha : a ∈ closure (S : Set R)) (hb : b ∈ closure (S : Set R)) : a * b ∈ closure (S : Set R)

Full source

/-- The product of two elements of the additive closure of a submonoid `M` is an element of the
additive closure of `M`. -/
lemma mul_mem_add_closure (ha : a ∈ closure (S : Set R))
    (hb : b ∈ closure (S : Set R)) : a * b ∈ closure (S : Set R) := by
  induction hb using closure_induction with
  | mem r hr => exact MulMemClass.mul_right_mem_add_closure ha hr
  | one => simp only [mul_zero, zero_mem _]
  | mul r s _ _ hr hs => simpa only [mul_add] using add_mem hr hs

Product of Elements in Additive Closure of Subsemigroup Belongs to Additive Closure

Informal description

Let $R$ be a non-unital non-associative semiring and $S$ a multiplicative subsemigroup of $R$. For any elements $a$ and $b$ in the additive closure of $S$, the product $a \cdot b$ is also contained in the additive closure of $S$.

MulMemClass.mul_left_mem_add_closure theorem

(ha : a ∈ S) (hb : b ∈ closure (S : Set R)) : a * b ∈ closure (S : Set R)

Full source

/-- The product of an element of `S` and an element of the additive closure of a multiplicative
submonoid `S` is contained in the additive closure of `S`. -/
lemma mul_left_mem_add_closure (ha : a ∈ S) (hb : b ∈ closure (S : Set R)) :
    a * b ∈ closure (S : Set R) :=
  mul_mem_add_closure (AddSubmonoid.mem_closure.mpr fun _sT hT => hT ha) hb

Left multiplication by subsemigroup element preserves additive closure

Informal description

Let $R$ be a non-unital non-associative semiring and $S$ a multiplicative subsemigroup of $R$. For any element $a \in S$ and any element $b$ in the additive closure of $S$, the product $a \cdot b$ is contained in the additive closure of $S$.