case zero
K : Type ?u.893582
R : Type ?u.893585
x : (ZMod Nat.zero)ˣ
⊢ x ^ φ Nat.zero = 1

case succ
K : Type ?u.893582
R : Type ?u.893585
n✝ : ℕ
x : (ZMod (Nat.succ n✝))ˣ
⊢ x ^ φ (Nat.succ n✝) = 1
K : Type ?u.893582
R : Type ?u.893585
n : ℕ
x : (ZMod n)ˣ
⊢ x ^ φ n = 1
cases n
no goals
case zero
K : Type ?u.893582
R : Type ?u.893585
x : (ZMod Nat.zero)ˣ
⊢ x ^ φ Nat.zero = 1
rw [Nat.totient_zero, pow_zero]
no goals
case succ
K : Type ?u.893582
R : Type ?u.893585
n✝ : ℕ
x : (ZMod (Nat.succ n✝))ˣ
⊢ x ^ φ (Nat.succ n✝) = 1
rw [← card_units_eq_totient, pow_card_eq_one]