case zero
K : Type ?u.1002572
R : Type ?u.1002575
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
⊢ x ^ p ^ Nat.zero = x

case succ
K : Type ?u.1002572
R : Type ?u.1002575
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
n : ℕ
ih : x ^ p ^ n = x
⊢ x ^ p ^ Nat.succ n = x
K : Type ?u.1002572
R : Type ?u.1002575
n p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
⊢ x ^ p ^ n = x
induction' n with n ih
no goals
case zero
K : Type ?u.1002572
R : Type ?u.1002575
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
⊢ x ^ p ^ Nat.zero = x
simp
no goals
case succ
K : Type ?u.1002572
R : Type ?u.1002575
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
n : ℕ
ih : x ^ p ^ n = x
⊢ x ^ p ^ Nat.succ n = x
simp [pow_succ, pow_mul, ih, pow_card]