Commit 2025-10-11 20:21 f9f5e911

View on Github →

feat(NumberTheory/ArithmeticFunction): add some lemmas (#30147) feat(NumberTheory/ArithmeticFunction): add a few lemmas:

ζ commutes with everything
f.ppow 1 = f and pow 1 = id
An expression for σ using prime factorization, generalizing Nat.sum_divisors

Estimated changes

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

added theorem ArithmeticFunction.coe_zeta_mul_comm

added theorem ArithmeticFunction.pow_one_eq_id

added theorem ArithmeticFunction.ppow_one

added theorem ArithmeticFunction.sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul

added theorem ArithmeticFunction.zeta_mul_comm