Theorem Nat.primeFactorsList_ne_nil

Modification history

2025-08-27 05:29
Mathlib/Data/Nat/Factors.lean
feat(NumberTheory/ArithmeticFunction): some additional theorems for `cardFactors` (`Ω`) (#28941)
Added Nat.primeFactorsList_ne_nilView on Github →