English
The product of two elements from the additive closure of a multiplicative submonoid S remains in the additive closure of S.
Русский
Произведение двух элементов аддитивного замыкания подморси S остается в аддитивном замыкании S.
LaTeX
$$$a \in \overline{S} \land b \in \overline{S} \Rightarrow ab \in \overline{S}$$$
Lean4
/-- The product of two elements of the additive closure of a submonoid `M` is an element of the
additive closure of `M`. -/
theorem 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
| zero => simp only [mul_zero, zero_mem _]
| add r s _ _ hr hs => simpa only [mul_add] using add_mem hr hs
