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

case inr
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : IsEmpty n
⊢ charpoly (M ^ Fintype.card K) = charpoly M
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
⊢ charpoly (M ^ Fintype.card K) = charpoly M
cases (isEmpty_or_nonempty n).symm
case inl.intro
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp : CharP K p
⊢ charpoly (M ^ Fintype.card K) = charpoly M
case inl
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
⊢ charpoly (M ^ Fintype.card K) = charpoly M
cases' CharP.exists K with p hp
case inl.intro
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp : CharP K p
this : CharP K p := hp
⊢ charpoly (M ^ Fintype.card K) = charpoly M
case inl.intro
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp : CharP K p
⊢ charpoly (M ^ Fintype.card K) = charpoly M
letI := hp
case inl.intro.intro.mk.intro
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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 ^ ↑{ val := k, property := kpos }
⊢ charpoly (M ^ Fintype.card K) = charpoly M
case inl.intro
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp : CharP K p
this : CharP K p := hp
⊢ charpoly (M ^ Fintype.card K) = charpoly M
rcases FiniteField.card K p with ⟨⟨k, kpos⟩, ⟨hp, hk⟩⟩
case inl.intro.intro.mk.intro
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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 ^ ↑{ val := k, property := kpos }
this : Fact (Nat.Prime p)
⊢ charpoly (M ^ Fintype.card K) = charpoly M
case inl.intro.intro.mk.intro
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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 ^ ↑{ val := k, property := kpos }
⊢ charpoly (M ^ Fintype.card K) = charpoly M
haveI : Fact p.Prime := ⟨hp⟩
case inl.intro.intro.mk.intro
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)
⊢ charpoly (M ^ Fintype.card K) = charpoly M
case inl.intro.intro.mk.intro
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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 ^ ↑{ val := k, property := kpos }
this : Fact (Nat.Prime p)
⊢ charpoly (M ^ Fintype.card K) = charpoly M
dsimp at hk
case inl.intro.intro.mk.intro
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)
⊢ charpoly (M ^ p ^ k) = charpoly M
case inl.intro.intro.mk.intro
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)
⊢ charpoly (M ^ Fintype.card K) = charpoly M
rw [hk]
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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]) (charpoly (M ^ p ^ k)) = (↑(frobenius K[X] p)^[k]) (charpoly M)
case inl.intro.intro.mk.intro
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)
⊢ charpoly (M ^ p ^ k) = charpoly M
apply (frobenius_inj K[X] p).iterate k
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)
⊢ charpoly (M ^ Fintype.card K) ^ Fintype.card K = charpoly M ^ Fintype.card K
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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]) (charpoly (M ^ p ^ k)) = (↑(frobenius K[X] p)^[k]) (charpoly M)
repeat' rw [iterate_frobenius (R := K[X])]; rw [← hk]
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)) (charpoly (M ^ Fintype.card K)) = charpoly M ^ Fintype.card K
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)
⊢ charpoly (M ^ Fintype.card K) ^ Fintype.card K = charpoly M ^ Fintype.card K
rw [← FiniteField.expand_card]
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)) (det (charmatrix (M ^ Fintype.card K))) = det (charmatrix M) ^ Fintype.card K
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)) (charpoly (M ^ Fintype.card K)) = charpoly M ^ Fintype.card K
unfold charpoly
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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 (↑(AlgHom.mapMatrix (expand K (Fintype.card K))) (charmatrix (M ^ Fintype.card K))) =
    ↑detMonoidHom (charmatrix M ^ Fintype.card K)
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)) (det (charmatrix (M ^ Fintype.card K))) = det (charmatrix M) ^ Fintype.card K
rw [AlgHom.map_det, ← coe_detMonoidHom, ← (detMonoidHom : Matrix n n K[X] →* K[X]).map_pow]
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)
⊢ ↑(AlgHom.mapMatrix (expand K (Fintype.card K))) (charmatrix (M ^ Fintype.card K)) = charmatrix M ^ Fintype.card K
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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 (↑(AlgHom.mapMatrix (expand K (Fintype.card K))) (charmatrix (M ^ Fintype.card K))) =
    ↑detMonoidHom (charmatrix M ^ Fintype.card K)
apply congr_arg det
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)
⊢ ↑matPolyEquiv (↑(AlgHom.mapMatrix (expand K (Fintype.card K))) (charmatrix (M ^ Fintype.card K))) =
    ↑matPolyEquiv (charmatrix M ^ Fintype.card K)
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)
⊢ ↑(AlgHom.mapMatrix (expand K (Fintype.card K))) (charmatrix (M ^ Fintype.card K)) = charmatrix M ^ Fintype.card K
refine' matPolyEquiv.injective _
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)
⊢ ↑matPolyEquiv (↑(AlgHom.mapMatrix (expand K (p ^ k))) (charmatrix (M ^ p ^ k))) = X ^ p ^ k - ↑C (M ^ p ^ k)

case inl.intro.intro.mk.intro.a.h
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)
⊢ ↑matPolyEquiv (↑(AlgHom.mapMatrix (expand K (Fintype.card K))) (charmatrix (M ^ Fintype.card K))) =
    ↑matPolyEquiv (charmatrix M ^ Fintype.card K)
rw [AlgEquiv.map_pow, matPolyEquiv_charmatrix, hk, sub_pow_char_pow_of_commute, ← C_pow]
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)
⊢ charpoly (M ^ Fintype.card K) ^ Fintype.card K = charpoly M ^ Fintype.card K
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)
⊢ charpoly (M ^ Fintype.card K) ^ Fintype.card K = charpoly M ^ Fintype.card K
rw [iterate_frobenius (R := K[X])]
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)
⊢ charpoly (M ^ Fintype.card K) ^ Fintype.card K = charpoly M ^ Fintype.card K
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)
⊢ charpoly (M ^ Fintype.card K) ^ Fintype.card K = charpoly M ^ p ^ k
rw [← hk]
no goals
case inl.intro.intro.mk.intro.a
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)
⊢ ↑matPolyEquiv (↑(AlgHom.mapMatrix (expand K (p ^ k))) (charmatrix (M ^ p ^ k))) = X ^ p ^ k - ↑C (M ^ p ^ k)
exact (id (matPolyEquiv_eq_x_pow_sub_c (p ^ k) M) : _)
no goals
case inl.intro.intro.mk.intro.a.h
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
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)
exact (C M).commute_X
no goals
case inr
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : IsEmpty n
⊢ charpoly (M ^ Fintype.card K) = charpoly M
exact congr_arg _ (Subsingleton.elim _ _)