Mathlib Changelog
v4
Changelog
About
Github
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