theorem proved term proof

`rs_riemannZeta_eulerProduct_tprod`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  38theorem rs_riemannZeta_eulerProduct_tprod (s : ℂ) (hs : 1 < s.re) :
  39    ∏' p : Nat.Primes, (1 - (p : ℂ) ^ (-s))⁻¹ = riemannZeta s :=

Term-mode proof.

  40  _root_.riemannZeta_eulerProduct_tprod hs
  41
  42/-- `HasProd` form of the same theorem. -/

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
Primes in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use