Theorems · Theorem · commutative algebra

MulMemClass.mul_right_mem_add_closure

∀ {M : Type u_1} {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst_1 : SetLike M R] [MulMemClass M R] {S : M}
  {a b : R}, a ∈ AddSubmonoid.closure ↑S → b ∈ S → a * b ∈ AddSubmonoid.closure ↑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.

Defined in

Mathlib.Algebra.Ring.Submonoid.Basic

Cited by

1 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NonUnitalNonAssocSemiringSetLikeMulMemClass