English
The product of an element a from the additive closure of a multiplicative subsemigroup S and an element b ∈ S lies in the additive closure of S.
Русский
Произведение элемента a из аддитивного замыкания множества S и элемента b из S принадлежит аддитивному замыканию S.
LaTeX
$$$a \in \overline{S} \land b \in S \Rightarrow ab \in \overline{S}$$$
Lean4
/-- 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 mul_right_mem_add_closure (ha : a ∈ closure (S : Set R)) (hb : b ∈ S) : a * b ∈ closure (S : Set R) := by
induction ha using closure_induction with
| mem r hr => exact mem_closure.mpr fun y hy => hy (mul_mem hr hb)
| zero => simp only [zero_mul, zero_mem _]
| add r s _ _ hr hs => simpa only [add_mul] using add_mem hr hs
