Registry ยท Proposition III.P07 tau-effective formalized

III.P07 โ€” Adelic Euler Product

ฯ„-holomorphic function on ๐”ธ_ฯ„ decomposes into local factors at each prime. Adelic form of Euler product: CRT lifted to holomorphic level.

Book III Part 3 Ch. 17

Dependency Graph

Depends on (2)

III.D22 III.T10

Lean Formalization

Module: TauLib.BookIII.Spectral.Adeles

Symbol: euler_product_check