no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ ↑normalize (lcm 0) = lcm 0
simp
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s✝ : Multiset α
a : α
s : Multiset α
x✝ : ↑normalize (lcm s) = lcm s
⊢ ↑normalize (lcm (a ::ₘ s)) = lcm (a ::ₘ s)
simp