Commit 2026-09-10 14:29 edbb3ee7
View on Github →refactor(Data/Nat/Factorization/Defs): redefine Nat.factorization in terms of primeFactorsList instead of padicValNat (#43581)
This PR redefines Nat.factorization in terms of primeFactorsList instead of padicValNat. This will allow Nat.factorization to remain computable even as padicValNat is deprecated in favor of the non-computable multiplicity.