∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {x : α} (n : ℕ),
  UniqueFactorizationMonoid.normalizedFactors (x ^ n) = n • UniqueFactorizationMonoid.normalizedFactors x