Theorems · Theorem · commutative algebra

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

Defined in

Mathlib.Algebra.Ring.Submonoid.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocSemiringSetLikeMulMemClass