Def Nat.primeFactors

Modification history

2024-07-17 17:39

Mathlib/Data/Nat/PrimeFin.lean

chore: Rename `Nat.factors` to `Nat.primeFactorsList` (#13832) …

Modified Nat.primeFactors View on Github →

2024-05-14 17:58

Mathlib/Data/Nat/PrimeFin.lean

chore: deprecate `@[pp_dot]` (#12609) …

Modified Nat.primeFactors View on Github →

2023-11-10 09:14

Mathlib/Data/Nat/PrimeFin.lean

refactor: Unify spelling of "prime factors" (#8164) …

Added Nat.primeFactors View on Github →