case intro
K : Type u_1
R : Type ?u.820624
inst✝³ : Field K
inst✝² : Fintype K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : Algebra (ZMod p✝) K
f : K[X]
p : ℕ
hp : CharP K p
⊢ ↑(expand K q) f = f ^ q
K : Type u_1
R : Type ?u.820624
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
f : K[X]
⊢ ↑(expand K q) f = f ^ q
cases' CharP.exists K with p hp
case intro
K : Type u_1
R : Type ?u.820624
inst✝³ : Field K
inst✝² : Fintype K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : Algebra (ZMod p✝) K
f : K[X]
p : ℕ
hp : CharP K p
this : CharP K p := hp
⊢ ↑(expand K q) f = f ^ q
case intro
K : Type u_1
R : Type ?u.820624
inst✝³ : Field K
inst✝² : Fintype K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : Algebra (ZMod p✝) K
f : K[X]
p : ℕ
hp : CharP K p
⊢ ↑(expand K q) f = f ^ q
letI := hp
case intro.intro.mk.intro
K : Type u_1
R : Type ?u.820624
inst✝³ : Field K
inst✝² : Fintype K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : Algebra (ZMod p✝) K
f : K[X]
p : ℕ
hp✝ : CharP K p
this : CharP K p := hp✝
n : ℕ
npos : 0 < n
hp : Nat.Prime p
hn : q = p ^ ↑{ val := n, property := npos }
⊢ ↑(expand K q) f = f ^ q
case intro
K : Type u_1
R : Type ?u.820624
inst✝³ : Field K
inst✝² : Fintype K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : Algebra (ZMod p✝) K
f : K[X]
p : ℕ
hp : CharP K p
this : CharP K p := hp
⊢ ↑(expand K q) f = f ^ q
rcases FiniteField.card K p with ⟨⟨n, npos⟩, ⟨hp, hn⟩⟩
case intro.intro.mk.intro
K : Type u_1
R : Type ?u.820624
inst✝³ : Field K
inst✝² : Fintype K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : Algebra (ZMod p✝) K
f : K[X]
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
n : ℕ
npos : 0 < n
hp : Nat.Prime p
hn : q = p ^ ↑{ val := n, property := npos }
this : Fact (Nat.Prime p)
⊢ ↑(expand K q) f = f ^ q
case intro.intro.mk.intro
K : Type u_1
R : Type ?u.820624
inst✝³ : Field K
inst✝² : Fintype K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : Algebra (ZMod p✝) K
f : K[X]
p : ℕ
hp✝ : CharP K p
this : CharP K p := hp✝
n : ℕ
npos : 0 < n
hp : Nat.Prime p
hn : q = p ^ ↑{ val := n, property := npos }
⊢ ↑(expand K q) f = f ^ q
haveI : Fact p.Prime := ⟨hp⟩
case intro.intro.mk.intro
K : Type u_1
R : Type ?u.820624
inst✝³ : Field K
inst✝² : Fintype K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : Algebra (ZMod p✝) K
f : K[X]
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
n : ℕ
npos : 0 < n
hp : Nat.Prime p
hn : q = p ^ n
this : Fact (Nat.Prime p)
⊢ ↑(expand K q) f = f ^ q
case intro.intro.mk.intro
K : Type u_1
R : Type ?u.820624
inst✝³ : Field K
inst✝² : Fintype K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : Algebra (ZMod p✝) K
f : K[X]
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
n : ℕ
npos : 0 < n
hp : Nat.Prime p
hn : q = p ^ ↑{ val := n, property := npos }
this : Fact (Nat.Prime p)
⊢ ↑(expand K q) f = f ^ q
dsimp at hn
no goals
case intro.intro.mk.intro
K : Type u_1
R : Type ?u.820624
inst✝³ : Field K
inst✝² : Fintype K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : Algebra (ZMod p✝) K
f : K[X]
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
n : ℕ
npos : 0 < n
hp : Nat.Prime p
hn : q = p ^ n
this : Fact (Nat.Prime p)
⊢ ↑(expand K q) f = f ^ q
rw [hn, ← map_expand_pow_char, frobenius_pow hn, RingHom.one_def, map_id]