Commit 2025-10-07 12:53 98c8639e

View on Github →

refactor: Nat.minFac: avoid reducing wfrec (#30291)

Estimated changes

Modified Mathlib/Data/Nat/Prime/Defs.lean

modified def Nat.minFacAux

Modified Mathlib/Data/Num/Prime.lean