-- Mathlib/LinearAlgebra/Matrix/Charpoly/FiniteField.lean
theorem FiniteField.Matrix.charpoly_pow_card {K : Type*} [Field K] [Fintype K] (M : Matrix n n K) :
    (M ^ Fintype.card K).charpoly = M.charpoly

Proof state:
case inr
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : IsEmpty n
⊢ (M ^ Fintype.card K).charpoly = M.charpoly

Tactic:
exact congr_arg _ (Subsingleton.elim _ _)

Result:
no goals

Proof state:
case inl.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp : CharP K p
⊢ (M ^ Fintype.card K).charpoly = M.charpoly

Tactic:
letI := hp

Result:
case inl.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp : CharP K p
this : CharP K p := hp
⊢ (M ^ Fintype.card K).charpoly = M.charpoly

Proof state:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (M ^ Fintype.card K).charpoly ^ Fintype.card K = M.charpoly ^ p ^ k

Tactic:
rw [← hk]

Result:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (M ^ Fintype.card K).charpoly ^ Fintype.card K = M.charpoly ^ Fintype.card K

Proof state:
case inl.intro.intro.mk.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (M ^ Fintype.card K).charpoly = M.charpoly

Tactic:
rw [hk]

Result:
case inl.intro.intro.mk.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (M ^ p ^ k).charpoly = M.charpoly

Proof state:
case inl.intro.intro.mk.intro.a.h
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ Commute X (C M)

Tactic:
exact (C M).commute_X

Result:
no goals

Proof state:
case inl.intro.intro.mk.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ ↑⟨k, kpos⟩
this : Fact (Nat.Prime p)
⊢ (M ^ Fintype.card K).charpoly = M.charpoly

Tactic:
dsimp at hk

Result:
case inl.intro.intro.mk.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (M ^ Fintype.card K).charpoly = M.charpoly

Proof state:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (⇑(frobenius K[X] p))^[k] (M ^ p ^ k).charpoly = (⇑(frobenius K[X] p))^[k] M.charpoly

Tactic:
repeat' rw [iterate_frobenius (R := K[X])]; rw [← hk]

Result:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (M ^ Fintype.card K).charpoly ^ Fintype.card K = M.charpoly ^ Fintype.card K

Proof state:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (M ^ Fintype.card K).charpoly ^ Fintype.card K = (⇑(frobenius K[X] p))^[k] M.charpoly

Tactic:
rw [iterate_frobenius (R := K[X])]

Result:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (M ^ Fintype.card K).charpoly ^ Fintype.card K = M.charpoly ^ p ^ k

Proof state:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (expand K (Fintype.card K)) (M ^ Fintype.card K).charmatrix.det = M.charmatrix.det ^ Fintype.card K

Tactic:
rw [AlgHom.map_det, ← coe_detMonoidHom, ← (detMonoidHom : Matrix n n K[X] →* K[X]).map_pow]

Result:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ detMonoidHom ((expand K (Fintype.card K)).mapMatrix (M ^ Fintype.card K).charmatrix) =
    detMonoidHom (M.charmatrix ^ Fintype.card K)

Proof state:
case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
⊢ (M ^ Fintype.card K).charpoly = M.charpoly

Tactic:
obtain ⟨p, hp⟩ := CharP.exists K

Result:
case inl.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp : CharP K p
⊢ (M ^ Fintype.card K).charpoly = M.charpoly

Proof state:
case inl.intro.intro.mk.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (M ^ p ^ k).charpoly = M.charpoly

Tactic:
apply (frobenius_inj K[X] p).iterate k

Result:
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (⇑(frobenius K[X] p))^[k] (M ^ p ^ k).charpoly = (⇑(frobenius K[X] p))^[k] M.charpoly