Commit 2024-07-22 03:05 bec18f79

View on Github →

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

Estimated changes

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

added theorem ArithmeticFunction.sigma_apply_prime_pow

added theorem ArithmeticFunction.sigma_one_apply_prime_pow

added theorem Nat.Coprime.card_divisors_mul

added theorem Nat.Coprime.sum_divisors_mul

added theorem Nat.sum_divisors