Theorems · Theorem · number theory

ArithmeticFunction.ofPowerSeries_apply

∀ {R : Type u_1} [inst : CommSemiring R] {q : ℕ},
  1 < q →
    ∀ (f : PowerSeries R) (n : ℕ),
      ((ArithmeticFunction.ofPowerSeries q) f) n =
        Function.extend (fun x => q ^ x) (fun x => (PowerSeries.coeff x) f) 0 n

Defined in

Mathlib.NumberTheory.ArithmeticFunction.LFunction

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommSemiring