exact Associated.refl _
case intro
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
this : Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a
m : ℕ
hm : evenFactorExp a = 2 * m
⊢ Associated (4 ^ m * Multiset.prod (oddFactors a)) ((2 ^ 2) ^ m * Multiset.prod (oddFactors a))
no goals