Theorems · Theorem · number theory

ArithmeticFunction.isMultiplicative_ofPowerSeries_of_isPrimePow

∀ {R : Type u_1} [inst : CommRing R] (q : ℕ),
  IsPrimePow q →
    ∀ (f : PowerSeries R), PowerSeries.constantCoeff f = 1 → ((ArithmeticFunction.ofPowerSeries q) f).IsMultiplicative

ArithmeticFunction.ofPowerSeries produces multiplicative power series.

Defined in: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Cited by: 0 results in Mathlib
Foundations: Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites34

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
RingHom.idproof · cited by 18,349
CommRingstatement and proof · cited by 17,173
CommSemiringproof · cited by 10,911
RingHomstatement · cited by 10,189
mul_oneproof · cited by 3,885
AlgHomstatement · cited by 3,236
one_mulproof · cited by 2,841
MulZeroClass.mul_zeroproof · cited by 2,091
MulZeroClass.zero_mulproof · cited by 1,625
LT.lt.ne'proof · cited by 1,417
pow_zeroproof · cited by 1,094

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.