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