Theorem tsum_pow_div_one_sub_eq_tsum_sigma

Modification history

2025-12-27 18:03
Mathlib/NumberTheory/TsumDivisorsAntidiagonal.lean
feat(NumberTheory/ModularForms/EisensteinSeries/Summable): add auxiliary E2 lemmas (#32955) …
Modified tsum_pow_div_one_sub_eq_tsum_sigmaView on Github →
2025-09-08 19:22
Mathlib/NumberTheory/TsumDivsorsAntidiagonal.lean
feat(NumberTheory/Divisors): divisors antidiagonal tsum (#28690)
Added tsum_pow_div_one_sub_eq_tsum_sigmaView on Github →