no goals
ι✝ : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
ι : Type u_1
s : Finset ι
x : ι → A
⊢ ∏ i in s, span R {x i} = span R {∏ i in s, x i}
rw [prod_span, Set.finset_prod_singleton]