Actual unit permutations · independently counted totients · Constructive arithmetic

Euler's theorem for units

m>1 ∧ Unit(a,m) ∧ Phi(m,t) ⇒ ∃w. Pow(a,t,w) ∧ ModEq(m,w,1)

Follow the constructed multiplier permutation, the weighted finite product, and the count-prefix induction to an actual power congruent to one.

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

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 certificate

Fully expanded arithmetic

Inspect all 1203 native tactic lines and 91 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem EU0022 and follow only the lemmas and conservative definitions supporting euler_theorem_for_units.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G014 milestone → theorem and definition dependencies.
Major independently established statements: EU000D euler_multiplier_permutation_exists · EU0017 euler_unit_product_coprime · EU001E euler_unit_count_product_balance · EU0020 euler_coprime_totient_power · EU0022 euler_theorem_for_units.
Independently verified Alpha v34 checked-use theorem family: 32 dependency-curried kernel-checked theorem bodies · 91 proof prerequisites · 23 linked definitions · 40 definition-dependency arrows · 1203 exact tactic lines · first admitted v31 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 210 bundle nodes; SHA-256 1edfcb7021a0869c2493383c75dea367d757be0b77f36fc6ad3f5fd18ed38210.
Exact mathematical boundary: The exact G014 theorem covers m>1 and genuinely invertible a. Phi counts coprime residues independently of the conclusion. The broader coprime theorem handles m=1 by congruence, not by asserting that one is a canonical remainder. Multiplicative-order and RSA statements are not claimed.