Commit 2025-09-08 19:22 9d6c05be

View on Github →

feat(NumberTheory/Divisors): divisors antidiagonal tsum (#28690)

Estimated changes

Modified Mathlib/Analysis/Asymptotics/Lemmas.lean

added theorem Summable.mul_tendsto_const

Modified Mathlib/Analysis/Complex/Exponential.lean

Modified Mathlib/Analysis/Complex/Norm.lean

modified theorem Complex.nnnorm_natCast

Modified Mathlib/Analysis/Normed/Group/Basic.lean

modified theorem Real.norm_natCast

Modified Mathlib/Analysis/Normed/Group/Int.lean

Modified Mathlib/Analysis/Normed/Module/Basic.lean

added theorem norm_natCast

Modified Mathlib/Analysis/RCLike/Basic.lean

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

added theorem ArithmeticFunction.sigma_eq_sum_div

Modified Mathlib/NumberTheory/TsumDivsorsAntidiagonal.lean

added theorem summable_norm_pow_mul_geometric_div_one_sub

added theorem summable_prod_mul_pow

added theorem tsum_pow_div_one_sub_eq_tsum_sigma

added theorem tsum_prod_pow_eq_tsum_sigma

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

added theorem tprod_congr₂