Coprime-residue counts · prime-power blocks · distinct-prime products · Constructive arithmetic

Euler's totient product formula

n>0 ⇒ ∃t. Phi(n,t) ∧ t=∏ over distinct p∣n of p^(vₚ(n)−1)(p−1)

Prove the equality between an actual count of coprime residues and an independently computed Euler product.

Open the definition-aware map Read the final theorem See campaign milestone G006

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact certificate

Fully expanded arithmetic

Inspect all 3206 native tactic lines and 266 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem TP0054 and follow only the lemmas and conservative definitions supporting totient_euler_product_formula.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G006 milestone → theorem and definition dependencies.
Major independently established statements: TP0019 totient_exists_unique · TP003B totient_prime_power_value · TP003F totient_coprime_multiplicative · TP0052 totient_euler_product_one · TP0051 totient_euler_product_iff · TP0054 totient_euler_product_formula.
Independently verified Alpha v34 checked-use theorem family: 84 dependency-curried kernel-checked theorem bodies · 266 proof prerequisites · 25 linked definitions · 48 definition-dependency arrows · 3206 exact tactic lines · first admitted v29 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 566 bundle nodes; SHA-256 4fcb3cd45e83448776abb9e33692496a7acfa98a051cae15761826a0b15fda44.
Exact mathematical boundary: Phi counts the actual 0/1 coprimality bits on 0≤a<n. EulerProduct has no Phi assumption or conclusion hidden in its definition. The empty product and the residue zero give Phi(1,1). The theorem does not assert Phi at zero.