Theorem: HTPI.Euler's_theorem (HTPILib/Chap7.lean)

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
⊢ ↑a ^ phi m ≡ 1 (MOD m)
Tactic:
have h2 : [a]_m ^ (phi m) = [1]_m := Theorem_7_4_2 h1
State after:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : [↑a]_m ^ phi m = [1]_m
⊢ ↑a ^ phi m ≡ 1 (MOD m)

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : [↑a]_m ^ phi m = [1]_m
⊢ ↑a ^ phi m ≡ 1 (MOD m)
Tactic:
rewrite [Exercise_7_4_5_Nat m a (phi m)] at h2
State after:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : [↑a ^ phi m]_m = [1]_m
⊢ ↑a ^ phi m ≡ 1 (MOD m)

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : [↑a ^ phi m]_m = [1]_m
⊢ ↑a ^ phi m ≡ 1 (MOD m)
Tactic:
show a ^ (phi m) ≡ 1 (MOD m) from (cc_eq_iff_congr _ _ _).ltr h2
State after:
no goals