no goals
R : Type u
ι : Type ?u.251146
inst✝ : CommSemiring R
I J K L : Ideal R
m : Multiset R
⊢ Multiset.prod (Multiset.map (fun x => span {x}) 0) = span {Multiset.prod 0}
simp
no goals
R : Type u
ι : Type ?u.251146
inst✝ : CommSemiring R
I J K L : Ideal R
m✝ : Multiset R
a : R
m : Multiset R
ih : Multiset.prod (Multiset.map (fun x => span {x}) m) = span {Multiset.prod m}
⊢ Multiset.prod (Multiset.map (fun x => span {x}) (a ::ₘ m)) = span {Multiset.prod (a ::ₘ m)}
simp only [Multiset.map_cons, Multiset.prod_cons, ih, ← Ideal.span_singleton_mul_span_singleton]