Theorems · Theorem · number theory

tprod_eq_tprod_primes_mul_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), f ↑p) * ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 2))

Defined in

Mathlib.NumberTheory.EulerProduct.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommGroupUniformSpaceIsUniformGroupCompleteSpaceT0Space