Lemmas about additive closures of Subsemigroup. #
theorem
MulMemClass.mul_right_mem_add_closure
{M : Type u_1}
{R : Type u_2}
[NonUnitalNonAssocSemiring R]
[SetLike M R]
[MulMemClass M R]
{S : M}
{a b : R}
(ha : a ∈ AddSubmonoid.closure ↑S)
(hb : b ∈ S)
:
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.
theorem
MulMemClass.mul_mem_add_closure
{M : Type u_1}
{R : Type u_2}
[NonUnitalNonAssocSemiring R]
[SetLike M R]
[MulMemClass M R]
{S : M}
{a b : R}
(ha : a ∈ AddSubmonoid.closure ↑S)
(hb : b ∈ AddSubmonoid.closure ↑S)
:
The product of two elements of the additive closure of a submonoid M is an element of the
additive closure of M.
theorem
MulMemClass.mul_left_mem_add_closure
{M : Type u_1}
{R : Type u_2}
[NonUnitalNonAssocSemiring R]
[SetLike M R]
[MulMemClass M R]
{S : M}
{a b : R}
(ha : a ∈ S)
(hb : b ∈ AddSubmonoid.closure ↑S)
:
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.