Theorems · Theorem · number theory

tsum_pow_div_one_sub_eq_tsum_sigma

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormSMulClass ℤ 𝕜] {r : 𝕜},
  ‖r‖ < 1 →
    ∀ (k : ℕ), ∑' (n : ℕ+), ↑↑n ^ k * r ^ ↑n / (1 - r ^ ↑n) = ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma k) ↑n) * r ^ ↑n

Defined in

Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Cited by

1 results in Mathlib

Foundations

Depth 173 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldCompleteSpaceNormSMulClass