Commit 2025-08-27 05:29 237433f6

View on Github →

feat(NumberTheory/ArithmeticFunction): some additional theorems for cardFactors (Ω) (#28941)

Estimated changes

Modified Mathlib/Data/Nat/Factors.lean

added theorem Nat.primeFactorsList_ne_nil

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

added theorem ArithmeticFunction.cardFactors_eq_sum_factorization

added theorem ArithmeticFunction.cardFactors_eq_zero_iff_eq_zero_or_one

added theorem ArithmeticFunction.cardFactors_pos_iff_one_lt