Theorems · Theorem · commutative algebra

MulMemClass.mul_left_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 ∈ S → b ∈ AddSubmonoid.closure ↑S → a * 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.

Defined in

Mathlib.Algebra.Ring.Submonoid.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocSemiringSetLikeMulMemClass