Theorem ArithmeticFunction.sigma_one_apply_prime_pow

Modification history

2025-12-02 09:01

Mathlib/NumberTheory/ArithmeticFunction.lean

refactor(NumberTheory/ArithmeticFunction): split long file (#32304) …

Modified ArithmeticFunction.sigma_one_apply_prime_pow View on Github →

2024-07-22 03:05

Mathlib/NumberTheory/ArithmeticFunction.lean

feat(ArithmeticFunction): more corollaries of `isMultiplicative_sigma` (#14597)

Added ArithmeticFunction.sigma_one_apply_prime_pow View on Github →