rwa [prod_map_norm, prod_map_norm]
case a
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
⊢ Associated (Multiset.prod (Multiset.map Zsqrtd.norm f)) (Multiset.prod (Multiset.map Zsqrtd.norm g))
no goals