awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
hk : M ^ k = 0
h :
  1 =
    1 -
      HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X
          ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M : Matrix.{v, v, u} n n R[X]) ^
        k
h₁ :
  1 =
    1 -
      HPow.hPow (α := R[X]) X k •
        HPow.hPow (α := Matrix.{v, v, u} n n R[X])
          ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M : Matrix.{v, v, u} n n R[X]) k
h₂ :
  1 =
    1 -
      HSMul.hSMul (β := Matrix.{v, v, u} n n R[X]) (HPow.hPow (α := R[X]) X k)
        ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) (M ^ k) : Matrix.{v, v, u} n n R[X])
h₃ :
  1 =
    1 -
      HSMul.hSMul (β := Matrix.{v, v, u} n n R[X]) (HPow.hPow (α := R[X]) X k)
        ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) 0)
h₄ : 1 = 1 - HSMul.hSMul (β := Matrix.{v, v, u} n n R[X]) (HPow.hPow (α := R[X]) X k) 0
h₅ : 1 = HSub.hSub (α := Matrix.{v, v, u} n n R[X]) 1 0
h₆ h₇ : Eq (α := Matrix.{v, v, u} n n R[X]) 1 1
⊢ 1 = 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ^ k

Tactic:
rw [← C.mapMatrix_apply, smul_pow, ← map_pow, hk, map_zero, smul_zero, sub_zero]

Premises used: Polynomial.C, RingHom.mapMatrix_apply, sub_zero, smul_zero, map_zero, map_pow, smul_pow
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
hk : M ^ k = 0
⊢ 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ∣ 1

Tactic:
replace hk : 1 - (X : R[X]) • M.map C ∣ 1 := by
    convert! one_sub_dvd_one_sub_pow ((X : R[X]) • M.map C) k
    rw [← C.mapMatrix_apply, smul_pow, ← map_pow, hk, map_zero, smul_zero, sub_zero]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
hk : 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ∣ 1
h : Dvd.dvd (α := R[X]) M.charpolyRev 1
⊢ IsUnit (M := R[X]) M.charpolyRev

Tactic:
apply isUnit_of_dvd_one

Premises used: isUnit_of_dvd_one
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
hk : 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ∣ 1
h : Dvd.dvd (α := R[X]) M.charpolyRev (det.{u, v} (n := n) 1)
⊢ Dvd.dvd (α := R[X]) M.charpolyRev 1

Tactic:
rw [← det_one (R := R[X]) (n := n)]

Premises used: Matrix.det_one
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
hk : 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ∣ 1
⊢ Dvd.dvd (α := R[X]) M.charpolyRev (det.{u, v} (n := n) 1)

Tactic:
map_dvd detMonoidHom hk

Premises used: Matrix.detMonoidHom, Matrix.charpolyRev, map_dvd, Matrix.det
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
hk : 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ∣ 1
⊢ Dvd.dvd (α := R[X]) M.charpolyRev (det.{u, v} (n := n) 1)

Tactic:
exact map_dvd detMonoidHom hk

Premises used: Matrix.detMonoidHom, map_dvd
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
hM : IsNilpotent M
inl : IsEmpty n → IsNilpotent M.trace
inr : Nonempty n → IsNilpotent M.trace
⊢ IsNilpotent M.trace

Tactic:
cases isEmpty_or_nonempty n

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h : IsEmpty n
⊢ IsNilpotent M.trace

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h : Nonempty n
this : IsNilpotent (coeff M.charpolyRev 1)
⊢ IsNilpotent M.trace

Tactic:
simpa using this
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h : Nonempty n
inr : IsNilpotent (coeff M.charpolyRev 1)
⊢ IsNilpotent M.trace

Tactic:
suffices IsNilpotent (coeff (charpolyRev M) 1) by simpa using this
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h : Nonempty n
⊢ IsNilpotent (coeff M.charpolyRev 1)

Tactic:
(isUnit_iff_coeff_isUnit_isNilpotent.mp (isUnit_charpolyRev_of_isNilpotent hM)).2
    _ one_ne_zero

Premises used: Polynomial.isUnit_iff_coeff_isUnit_isNilpotent, And.right, Matrix.isUnit_charpolyRev_of_isNilpotent, Iff.mp, one_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h : Nonempty n
⊢ IsNilpotent (coeff M.charpolyRev 1)

Tactic:
exact (isUnit_iff_coeff_isUnit_isNilpotent.mp (isUnit_charpolyRev_of_isNilpotent hM)).2
    _ one_ne_zero

Premises used: Polynomial.isUnit_iff_coeff_isUnit_isNilpotent, And.right, Matrix.isUnit_charpolyRev_of_isNilpotent, Iff.mp, one_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
hM : IsNilpotent M
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h : Nontrivial R
p : R[X] := M.charpolyRev
rw : p %ₘ X + X * (p /ₘ X) - 1
| p - 1

Tactic:
rw [← modByMonic_add_div p X]

Premises used: Polynomial.modByMonic_add_div, Polynomial.X
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h : Nontrivial R
p : R[X] := M.charpolyRev
conv_lhs : p %ₘ X + X * (p /ₘ X) - 1 = X * (p /ₘ X)
⊢ p - 1 = X * (p /ₘ X)

Tactic:
conv_lhs => rw [← modByMonic_add_div p X]

Premises used: Polynomial.modByMonic_add_div, Polynomial.X
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h : Nontrivial R
p : R[X] := M.charpolyRev
⊢ p %ₘ X + X * (p /ₘ X) - 1 = X * (p /ₘ X)

Tactic:
simp [p, modByMonic_X]

Premises used: Polynomial.modByMonic_X
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h : Nontrivial R
p : R[X] := M.charpolyRev
⊢ p - 1 = X * (p /ₘ X)

Tactic:
have hp : p - 1 = X * (p /ₘ X) := by
    conv_lhs => rw [← modByMonic_add_div p X]
    simp [p, modByMonic_X]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h : Nontrivial R
p : R[X] := M.charpolyRev
hp : p - 1 = X * (p /ₘ X)
⊢ IsNilpotent (p /ₘ X)

Tactic:
have : IsNilpotent (p /ₘ X) :=
    (Polynomial.isUnit_iff'.mp (isUnit_charpolyRev_of_isNilpotent hM)).2
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h : Nontrivial R
p : R[X] := M.charpolyRev
hp : p - 1 = X * (p /ₘ X)
this : IsNilpotent (p /ₘ X)
⊢ max (natDegree M.charpoly) (HPow.hPow (α := R[X]) X (Fintype.card n)).natDegree ≤ natDegree M.charpoly

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h : Nontrivial R
p : R[X] := M.charpolyRev
hp : p - 1 = X * (p /ₘ X)
this : IsNilpotent (p /ₘ X)
⊢ (M.charpoly - HPow.hPow (α := R[X]) X (Fintype.card n)).natDegree ≤ natDegree M.charpoly

Tactic:
have aux : (M.charpoly - X ^ (Fintype.card n)).natDegree ≤ M.charpoly.natDegree :=
    le_trans (natDegree_sub_le _ _) (by simp)
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h : Nontrivial R
p : R[X] := M.charpolyRev
hp : p - 1 = X * (p /ₘ X)
this : IsNilpotent (p /ₘ X)
aux : (M.charpoly - HPow.hPow (α := R[X]) X (Fintype.card n)).natDegree ≤ natDegree M.charpoly
rw : IsNilpotent (M.charpolyRev - reflect (natDegree M.charpoly) (HPow.hPow (α := R[X]) X (Fintype.card n)))
⊢ IsNilpotent (M.charpoly - HPow.hPow (α := R[X]) X (Fintype.card n))

Tactic:
rw [← isNilpotent_reflect_iff aux, reflect_sub, ← reverse, M.reverse_charpoly]

Premises used: Polynomial.reflect_sub, Matrix.reverse_charpoly, Polynomial.isNilpotent_reflect_iff, Polynomial.reverse
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h : Nontrivial R
p : R[X] := M.charpolyRev
hp : p - 1 = X * (p /ₘ X)
this : IsNilpotent (p /ₘ X)
aux : (M.charpoly - HPow.hPow (α := R[X]) X (Fintype.card n)).natDegree ≤ natDegree M.charpoly
⊢ IsNilpotent (M.charpolyRev - reflect (natDegree M.charpoly) (HPow.hPow (α := R[X]) X (Fintype.card n)))

Tactic:
simpa [p, hp]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Disc
Goal:
R : Type u_1
n : Type u_2
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
g : GL n R
m : Matrix n n R
⊢ ((↑g : Matrix n n R) * m * (↑g : Matrix n n R)⁻¹).discr = m.discr

Tactic:
simp [discr]

Premises used: Matrix.discr
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Disc
Goal:
R : Type u_1
n : Type u_2
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
g : GL n R
m : Matrix n n R
⊢ ((↑g : Matrix n n R)⁻¹ * m * (↑g : Matrix n n R)).discr = m.discr

Tactic:
simp [discr]

Premises used: Matrix.discr
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Disc
Goal:
R : Type u_1
n : Type u_2
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n R
hn : Fintype.card n = 2
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Disc
Goal:
R : Type u_1
n : Type u_2
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n R
hn : Fintype.card n = 2
h : Nontrivial R
simp : Eq (α := WithBot ℕ) (↑(Fintype.card n) : WithBot ℕ) 2
⊢ degree A.charpoly = 2

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Disc
Goal:
R : Type u_1
n : Type u_2
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n R
hn : Fintype.card n = 2
h : Nontrivial R
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Fintype.card n = 2
⊢ Eq (α := WithBot ℕ) (↑(Fintype.card n) : WithBot ℕ) 2

Tactic:
norm_cast
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Disc
Goal:
R : Type u_1
n : Type u_2
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n R
hn : Fintype.card n = 2
h : Nontrivial R
rw :
  HPow.hPow (β := ℕ) (coeff A.charpoly 1) 2 - 4 * coeff A.charpoly 0 * coeff A.charpoly 2 =
    HPow.hPow (β := ℕ) A.trace 2 - 4 * A.det
⊢ A.discr = HPow.hPow (β := ℕ) A.trace 2 - 4 * A.det

Tactic:
rw [discr, Polynomial.discr_of_degree_eq_two (by simp; norm_cast)]

Premises used: Matrix.discr, Polynomial.discr_of_degree_eq_two
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Disc
Goal:
R : Type u_1
n : Type u_2
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n R
hn : Fintype.card n = 2
h : Nontrivial R
⊢ HPow.hPow (β := ℕ) (coeff A.charpoly 1) 2 - 4 * coeff A.charpoly 0 * coeff A.charpoly 2 =
    HPow.hPow (β := ℕ) A.trace 2 - 4 * A.det

Tactic:
simp [A.charpoly_of_card_eq_two hn]

Premises used: Matrix.charpoly_of_card_eq_two
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Disc
Goal:
R : Type u_1
inst : CommRing R
A : Matrix (Fin 2) (Fin 2) R
⊢ A.discr = HPow.hPow (β := ℕ) A.trace 2 - 4 * A.det

Tactic:
A.discr_of_card_eq_two <| Fintype.card_fin _

Premises used: Fintype.card_fin, Matrix.discr_of_card_eq_two
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : CommRing R
B : Matrix n n R
r : R
⊢ r ∈ spectrum R B ↔ ¬IsUnit (eval r B.charpoly)

Tactic:
simp [eval_charpoly, spectrum.mem_iff, isUnit_iff_isUnit_det, algebraMap_eq_diagonal,
    Pi.algebraMap_def]

Premises used: Matrix.algebraMap_eq_diagonal, Matrix.isUnit_iff_isUnit_det, spectrum.mem_iff, Matrix.eval_charpoly, Pi.algebraMap_def
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : CommRing R
B : Matrix n n R
inst_3 : Nontrivial R
r : R
hr : IsRoot B.charpoly r
⊢ r ∈ spectrum R B

Tactic:
simp [mem_spectrum_iff_not_isUnit_eval_charpoly, hr.eq_zero]

Premises used: Matrix.mem_spectrum_iff_not_isUnit_eval_charpoly, Polynomial.IsRoot.eq_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
K : Type u_3
inst_2 : Field K
A : Matrix n n K
r : K
⊢ r ∈ spectrum K A ↔ IsRoot A.charpoly r

Tactic:
simp [mem_spectrum_iff_not_isUnit_eval_charpoly]

Premises used: Matrix.mem_spectrum_iff_not_isUnit_eval_charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : CommRing R
B : Matrix n n R
inst_3 : IsDomain R
hAps : Splits B.charpoly
rw : HPow.hPow (α := R) (-1) (Fintype.card n) * coeff B.charpoly 0 = (roots B.charpoly).prod
rw₁ : HPow.hPow (α := R) (-1) (natDegree B.charpoly) * coeff B.charpoly 0 = (roots B.charpoly).prod
rw₂ :
  HPow.hPow (α := R) (-1) (natDegree B.charpoly) *
      (HPow.hPow (α := R) (-1) (natDegree B.charpoly) * (roots B.charpoly).prod) =
    (roots B.charpoly).prod
rw₃ :
  HPow.hPow (α := R) (-1) (natDegree B.charpoly) * HPow.hPow (α := R) (-1) (natDegree B.charpoly) *
      (roots B.charpoly).prod =
    (roots B.charpoly).prod
rw₄ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := R) (-1) (natDegree B.charpoly)) 2 * (roots B.charpoly).prod =
    (roots B.charpoly).prod
rw₅ : HPow.hPow (α := R) (β := ℕ) (-1) 2 ^ natDegree B.charpoly * (roots B.charpoly).prod = (roots B.charpoly).prod
rw₆ : HPow.hPow (α := R) 1 (natDegree B.charpoly) * (roots B.charpoly).prod = (roots B.charpoly).prod
rw₇ : 1 * (roots B.charpoly).prod = (roots B.charpoly).prod
rw₈ rw₉ : (roots B.charpoly).prod = (roots B.charpoly).prod
⊢ B.det = (roots B.charpoly).prod

Tactic:
rw [det_eq_sign_charpoly_coeff, ← charpoly_natDegree_eq_dim B,
    hAps.coeff_zero_eq_prod_roots_of_monic B.charpoly_monic, ← mul_assoc,
    ← pow_two, pow_right_comm, neg_one_sq, one_pow, one_mul]

Premises used: one_pow, pow_two, pow_right_comm, neg_one_sq, mul_assoc, Polynomial.Splits.coeff_zero_eq_prod_roots_of_monic, Matrix.charpoly_natDegree_eq_dim, Matrix.charpoly_monic, Matrix.det_eq_sign_charpoly_coeff, one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : CommRing R
B : Matrix n n R
inst_3 : IsDomain R
hAps : Splits B.charpoly
inl : ∀ (h : IsEmpty n), B.trace = (roots B.charpoly).sum
inr : Nonempty n → B.trace = (roots B.charpoly).sum
⊢ B.trace = (roots B.charpoly).sum

Tactic:
rcases isEmpty_or_nonempty n with h | _

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : CommRing R
B : Matrix n n R
inst_3 : IsDomain R
hAps : Splits B.charpoly
h : IsEmpty n
⊢ B.trace = (roots B.charpoly).sum

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : CommRing R
B : Matrix n n R
inst_3 : IsDomain R
hAps : Splits B.charpoly
h : Nonempty n
inr : -nextCoeff B.charpoly = (roots B.charpoly).sum
inr₁ : nextCoeff B.charpoly = -(roots B.charpoly).sum
inr₂ inr₃ : nextCoeff B.charpoly = nextCoeff B.charpoly
⊢ B.trace = (roots B.charpoly).sum

Tactic:
rw [trace_eq_neg_charpoly_nextCoeff, neg_eq_iff_eq_neg,
      ← hAps.nextCoeff_eq_neg_sum_roots_of_monic B.charpoly_monic]

Premises used: neg_eq_iff_eq_neg, Polynomial.Splits.nextCoeff_eq_neg_sum_roots_of_monic, Matrix.trace_eq_neg_charpoly_nextCoeff, Matrix.charpoly_monic
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
K : Type u_3
inst_2 : Field K
A : Matrix n n K
inst_3 : IsAlgClosed K
⊢ A.det = (roots A.charpoly).prod

Tactic:
det_eq_prod_roots_charpoly_of_splits (IsAlgClosed.splits A.charpoly)

Premises used: Matrix.det_eq_prod_roots_charpoly_of_splits, IsAlgClosed.splits, Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
K : Type u_3
inst_2 : Field K
A : Matrix n n K
inst_3 : IsAlgClosed K
⊢ A.trace = (roots A.charpoly).sum

Tactic:
trace_eq_sum_roots_charpoly_of_splits (IsAlgClosed.splits A.charpoly)

Premises used: Matrix.trace_eq_sum_roots_charpoly_of_splits, IsAlgClosed.splits, Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
inl : Nonempty n → Eq (α := K[X]) (M ^ Fintype.card K).charpoly M.charpoly
inr : IsEmpty n → Eq (α := K[X]) (M ^ Fintype.card K).charpoly M.charpoly
⊢ Eq (α := K[X]) (M ^ Fintype.card K).charpoly M.charpoly

Tactic:
cases (isEmpty_or_nonempty n).symm

Premises used: isEmpty_or_nonempty, Or.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
h : Nonempty n
inl : ∀ (p : ℕ) (hp : CharP K p), Eq (α := K[X]) (M ^ Fintype.card K).charpoly M.charpoly
⊢ Eq (α := K[X]) (M ^ Fintype.card K).charpoly M.charpoly

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

Premises used: CharP.exists
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
h : Nonempty n
p : ℕ
hp : CharP K p
inl :
  ∀ (k : ℕ) (kpos : 0 < k) (hp : Nat.Prime p)
    (hk : Fintype.card K = p ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) k kpos) : ℕ)),
    Eq (α := K[X]) (M ^ Fintype.card K).charpoly M.charpoly
⊢ Eq (α := K[X]) (M ^ Fintype.card K).charpoly M.charpoly

Tactic:
rcases FiniteField.card K p with ⟨⟨k, kpos⟩, ⟨hp, hk⟩⟩

Premises used: FiniteField.card
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
h : Nonempty n
p : ℕ
hp_1 : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) k kpos) : ℕ)
⊢ Fact (Nat.Prime p)

Tactic:
haveI : Fact p.Prime := ⟨hp⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
h : Nonempty n
p : ℕ
hp_1 : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
inl : Eq (α := K[X]) (M ^ p ^ k).charpoly M.charpoly
⊢ Eq (α := K[X]) (M ^ Fintype.card K).charpoly M.charpoly

Tactic:
rw [hk]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
h : Nonempty n
p : ℕ
hp_1 : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
inl :
  Eq (α := K[X]) ((⇑(frobenius K[X] p) : (a : K[X]) → K[X])^[k] (M ^ p ^ k).charpoly)
    ((⇑(frobenius K[X] p) : (a : K[X]) → K[X])^[k] M.charpoly)
⊢ Eq (α := K[X]) (M ^ p ^ k).charpoly M.charpoly

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

Premises used: Function.Injective.iterate, Polynomial, frobenius_inj
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
h : Nonempty n
p : ℕ
hp_1 : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
inl : HPow.hPow (α := K[X]) (M ^ p ^ k).charpoly (p ^ k) = (⇑(frobenius K[X] p) : (a : K[X]) → K[X])^[k] M.charpoly
⊢ Eq (α := K[X]) ((⇑(frobenius K[X] p) : (a : K[X]) → K[X])^[k] (M ^ p ^ k).charpoly)
    ((⇑(frobenius K[X] p) : (a : K[X]) → K[X])^[k] M.charpoly)

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

Premises used: iterate_frobenius
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
h : Nonempty n
p : ℕ
hp_1 : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
inl :
  HPow.hPow (α := K[X]) (M ^ Fintype.card K).charpoly (Fintype.card K) =
    (⇑(frobenius K[X] p) : (a : K[X]) → K[X])^[k] M.charpoly
⊢ HPow.hPow (α := K[X]) (M ^ p ^ k).charpoly (p ^ k) = (⇑(frobenius K[X] p) : (a : K[X]) → K[X])^[k] M.charpoly

Tactic:
rw [← hk]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
h : Nonempty n
p : ℕ
hp_1 : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
inl : HPow.hPow (α := K[X]) (M ^ Fintype.card K).charpoly (Fintype.card K) = HPow.hPow (α := K[X]) M.charpoly (p ^ k)
⊢ HPow.hPow (α := K[X]) (M ^ Fintype.card K).charpoly (Fintype.card K) =
    (⇑(frobenius K[X] p) : (a : K[X]) → K[X])^[k] M.charpoly

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

Premises used: iterate_frobenius
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
h : Nonempty n
p : ℕ
hp_1 : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
inl :
  HPow.hPow (α := K[X]) (M ^ Fintype.card K).charpoly (Fintype.card K) =
    HPow.hPow (α := K[X]) M.charpoly (Fintype.card K)
⊢ HPow.hPow (α := K[X]) (M ^ Fintype.card K).charpoly (Fintype.card K) = HPow.hPow (α := K[X]) M.charpoly (p ^ k)

Tactic:
rw [← hk]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
h : Nonempty n
p : ℕ
hp_1 : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
inl :
  HPow.hPow (α := K[X]) (M ^ Fintype.card K).charpoly (Fintype.card K) =
    HPow.hPow (α := K[X]) M.charpoly (Fintype.card K)
⊢ Eq (α := K[X]) ((⇑(frobenius K[X] p) : (a : K[X]) → K[X])^[k] (M ^ p ^ k).charpoly)
    ((⇑(frobenius K[X] p) : (a : K[X]) → K[X])^[k] M.charpoly)

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

Premises used: iterate_frobenius