English
Let R be a semiring with star operation and A a star-module; if r and a belong to the closure of the set {star s · s}, then r · a also belongs to that closure.
Русский
Пусть R задаёт полупрямую полугруппу с операцией звёздочка и A — модуль со звёздочкой; если r и a лежат в замыкании множества {star s · s}, то и r · a принадлежит тому же замыканию.
LaTeX
$$$\\\\text{If } r \\\\in \\, \mathrm{closure}(\\\\{\\\\star(s) \\\\cdot s \\\\mid \\\\ s \\\\in R\\\\}) \\\\text{ and } a \\\\in \\, \mathrm{closure}(\\\\{\\\\star(s) \\\\cdot s \\\\mid \\\\ s \\\\in R\\\\}), \\\\text{ then } r \\\\cdot a \\\\in \\, \\mathrm{closure}(\\\\{\\\\star(s) \\\\cdot s \\\\mid \\\\ s \\\\in R\\\\}).$$$
Lean4
theorem smul_mem_closure_star_mul {r : R} (hr : r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)) {a : A}
(ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)) :
r • a ∈ AddSubmonoid.closure (range fun s ↦ star s * s) := by
induction hr using AddSubmonoid.closure_induction with
| zero => simp
| add r₁ r₂ _ _ hr₁ hr₂ => simpa [add_smul] using add_mem hr₁ hr₂
| mem r hr =>
induction ha using AddSubmonoid.closure_induction with
| zero => simp
| add a₁ a₂ _ _ ha₁ ha₂ => simpa [smul_add] using add_mem ha₁ ha₂
| mem a ha =>
obtain ⟨r, rfl⟩ := hr
obtain ⟨a, rfl⟩ := ha
exact AddSubmonoid.subset_closure ⟨r • a, by simp [star_smul, smul_mul_smul_comm]⟩
