English
The span of a finite product of sets equals the product of their spans: span R (∏ i∈s M(i)) = ∏ i∈s span R (M(i)).
Русский
Замыкание по линейному ряду одной конечной произведения множеств равно произведению их замыканий: span R (∏ i∈s M(i)) = ∏ i∈s span R (M(i)).
LaTeX
$$$\prod_{i\in s} \mathrm{span}\,R (M(i)) = \mathrm{span}\,R \left(\prod_{i\in s} M(i)\right)$$$
Lean4
/-- `span` is a semiring homomorphism (recall multiplication is pointwise multiplication of subsets
on either side). -/
@[simps]
noncomputable def ringHom : SetSemiring A →+* Submodule R A
where
toFun s := Submodule.span R (SetSemiring.down s)
map_zero' := span_empty
map_one' := one_eq_span.symm
map_add' := span_union
map_mul' s t := by simp_rw [SetSemiring.down_mul, span_mul_span]
