Theorems · Theorem · number theory

tprod_eq_tprod_primes_of_mulSupport_subset_prime_powers

∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : UniformSpace α] [IsUniformGroup α] [CompleteSpace α] [T0Space α]
  {f : ℕ → α},
  Multipliable f →
    Function.mulSupport f ⊆ {n | IsPrimePow n} → ∏' (n : ℕ), f n = ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 1))

Defined in

Mathlib.NumberTheory.EulerProduct.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommGroupUniformSpaceIsUniformGroupCompleteSpaceT0Space