case a
K : Type u_1
R : Type ?u.742366
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
⊢ ↑(frobenius K p ^ n) x = ↑1 x
K : Type u_1
R : Type ?u.742366
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
⊢ frobenius K p ^ n = 1
ext x
case a
K : Type u_1
R : Type ?u.742366
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
⊢ ↑(frobenius K p ^ n) x = x ^ p ^ n
case a
K : Type u_1
R : Type ?u.742366
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
⊢ ↑(frobenius K p ^ n) x = ↑1 x
conv_rhs => rw [RingHom.one_def, RingHom.id_apply, ← pow_card x, hcard]
case a
K : Type u_1
R : Type ?u.742366
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ ↑(frobenius K p ^ n) x = x ^ p ^ n
case a
K : Type u_1
R : Type ?u.742366
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
⊢ ↑(frobenius K p ^ n) x = x ^ p ^ n
clear hcard
case a.zero
K : Type u_1
R : Type ?u.742366
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
⊢ ↑(frobenius K p ^ Nat.zero) x = x ^ p ^ Nat.zero

case a.succ
K : Type u_1
R : Type ?u.742366
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
n : ℕ
hn : ↑(frobenius K p ^ n) x = x ^ p ^ n
⊢ ↑(frobenius K p ^ Nat.succ n) x = x ^ p ^ Nat.succ n
case a
K : Type u_1
R : Type ?u.742366
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ ↑(frobenius K p ^ n) x = x ^ p ^ n
induction' n with n hn
no goals
case a.zero
K : Type u_1
R : Type ?u.742366
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
⊢ ↑(frobenius K p ^ Nat.zero) x = x ^ p ^ Nat.zero
simp
no goals
case a.succ
K : Type u_1
R : Type ?u.742366
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
n : ℕ
hn : ↑(frobenius K p ^ n) x = x ^ p ^ n
⊢ ↑(frobenius K p ^ Nat.succ n) x = x ^ p ^ Nat.succ n
rw [pow_succ, pow_succ', pow_mul, RingHom.mul_def, RingHom.comp_apply, frobenius_def, hn]