feat: port Data.PNat.Factors (#1830)

Co-authored-by: qawbecrdtey <qawbecrdtey@naver.com>
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Lukas Miaskiwskyi <lukas.mias@gmail.com>

Mathlib.lean

@@ -509,6 +509,7 @@ import Mathlib.Data.PFun
 import Mathlib.Data.PFunctor.Univariate.Basic
 import Mathlib.Data.PNat.Basic
 import Mathlib.Data.PNat.Defs
+import Mathlib.Data.PNat.Factors
 import Mathlib.Data.PNat.Find
 import Mathlib.Data.PNat.Interval
 import Mathlib.Data.PNat.Prime

Mathlib/Data/Nat/Prime.lean

@@ -768,6 +768,7 @@ theorem prime_iff_prime_int {p : ℕ} : p.Prime ↔ _root_.Prime (p : ℤ) :=
 /-- The type of prime numbers -/
 def Primes :=
   { p : ℕ // p.Prime }
+  deriving DecidableEq
 #align nat.primes Nat.Primes
 
 namespace Primes

Mathlib/Data/PNat/Basic.lean

@@ -278,7 +278,7 @@ end deprecated
 -- where the left `^ : ℕ+ → ℕ → ℕ+` was `monoid.has_pow`.
 -- Atm writing `m ^ n` means automatically `(↑m) ^ n`.
 @[simp, norm_cast]
-theorem pow_coe (m : ℕ+) (n : ℕ) : ((Monoid.Pow.pow m n : ℕ+) : ℕ) = (m : ℕ) ^ n :=
+theorem pow_coe (m : ℕ+) (n : ℕ) : ((Pow.pow m n : ℕ+) : ℕ) = (m : ℕ) ^ n :=
   rfl
 #align pnat.pow_coe PNat.pow_coe