Theorem: euler_theorem (RSAProject/rsaproject.lean)

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
⊢ ∀ (t : (ZMod (p * q))ˣ), t ^ φ (p * q) = 1
Tactic:
have h2: NeZero (p*q) := by
  apply ne_zero_product_of_primes hp hq
State after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
⊢ ∀ (t : (ZMod (p * q))ˣ), t ^ φ (p * q) = 1

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
⊢ ∀ (t : (ZMod (p * q))ˣ), t ^ φ (p * q) = 1
Tactic:
have h1: Fintype.card (ZMod (p*q))ˣ = Nat.totient (p*q) := by
  rw [ZMod.card_units_eq_totient]
State after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
h1 : Fintype.card (ZMod (p * q))ˣ = φ (p * q)
⊢ ∀ (t : (ZMod (p * q))ˣ), t ^ φ (p * q) = 1

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
h1 : Fintype.card (ZMod (p * q))ˣ = φ (p * q)
⊢ ∀ (t : (ZMod (p * q))ˣ), t ^ φ (p * q) = 1
Tactic:
intro t
State after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
h1 : Fintype.card (ZMod (p * q))ˣ = φ (p * q)
t : (ZMod (p * q))ˣ
⊢ t ^ φ (p * q) = 1

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
h1 : Fintype.card (ZMod (p * q))ˣ = φ (p * q)
t : (ZMod (p * q))ˣ
⊢ t ^ φ (p * q) = 1
Tactic:
rw [←orderOf_dvd_iff_pow_eq_one, ←h1]
State after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
h1 : Fintype.card (ZMod (p * q))ˣ = φ (p * q)
t : (ZMod (p * q))ˣ
⊢ orderOf t ∣ Fintype.card (ZMod (p * q))ˣ

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
h1 : Fintype.card (ZMod (p * q))ˣ = φ (p * q)
t : (ZMod (p * q))ˣ
⊢ orderOf t ∣ Fintype.card (ZMod (p * q))ˣ
Tactic:
apply lagrange_theorem
State after:
no goals

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
⊢ NeZero (p * q)
Tactic:
apply ne_zero_product_of_primes hp hq
State after:
no goals

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
⊢ Fintype.card (ZMod (p * q))ˣ = φ (p * q)
Tactic:
rw [ZMod.card_units_eq_totient]
State after:
no goals