Computing `Nat.primeFactors`

Stream: mathlib4

[Jeremy Tan]

Why can't I use decide or norm_num to compute Nat.primeFactors?

import Mathlib.RingTheory.Radical

/-- The radical of a natural number is the product of its prime factors.
This is computable, unlike `UniqueFactorizationMonoid.radical`. -/
def Nat.radical (n : ℕ) : ℕ :=
  ∏ p ∈ n.primeFactors, p

lemma radical_899 : Nat.radical 899 = 899 := by
  decide -- fails

[Julian Berman]

I think #Is there code for X? > Compute Nat.primeFactors has some prior discussion

[Jeremy Tan]

Ah, yes

import Mathlib.RingTheory.Radical
import Mathlib.Tactic.Simproc.Factors

/-- The radical of a natural number is the product of its prime factors.
This is computable, unlike `UniqueFactorizationMonoid.radical`. -/
def Nat.radical (n : ℕ) : ℕ :=
  ∏ p ∈ n.primeFactors, p

lemma yyy : Nat.radical 899 = 899 := by
  simp only [Nat.radical, Nat.primeFactors, Nat.primeFactorsList_ofNat]
  norm_num

[Miyahara Kō]

It's because Nat.primeFactorsList & Nat.minFacAux are irreducible.
with_unfolding_all resolves this:

lemma radical_899 : Nat.radical 899 = 899 := by
  with_unfolding_all decide

[Joachim Breitner]

Since https://github.com/leanprover/lean4/pull/7965 has landed, it would be reasonable for Mathlib to make Nat.primeFactorsList and Nat.minFacAux to be reducible again, so that decide works fine.