awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
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 M.trace
have inr : IsNilpotent (coeff M.charpolyRev 1)
Tactic: suffices IsNilpotent (coeff (charpolyRev M) 1) by simpa using this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (hypothesis)
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
⊢ IsNilpotent (M.charpoly - HPow.hPow (α := R[X]) X (Fintype.card n))
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
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
have rw : p %ₘ X + X * (p /ₘ X) - 1
Tactic: rw [← modByMonic_add_div p X]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
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)
have conv_lhs : p %ₘ X + X * (p /ₘ X) - 1 = X * (p /ₘ X)
Tactic: conv_lhs => rw [← modByMonic_add_div p X]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (hypothesis)
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
⊢ IsNilpotent (M.charpoly - HPow.hPow (α := R[X]) X (Fintype.card n))
have hp : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (hypothesis)
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 (M.charpoly - HPow.hPow (α := R[X]) X (Fintype.card n))
have this : IsNilpotent (p /ₘ X)
Tactic: have : IsNilpotent (p /ₘ X) :=
    (Polynomial.isUnit_iff'.mp (isUnit_charpolyRev_of_isNilpotent hM)).2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (hypothesis)
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)
⊢ IsNilpotent (M.charpoly - HPow.hPow (α := R[X]) X (Fintype.card n))
have aux : (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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
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.charpoly - HPow.hPow (α := R[X]) X (Fintype.card n))
have rw : IsNilpotent (M.charpolyRev - reflect (natDegree M.charpoly) (HPow.hPow (α := R[X]) X (Fintype.card n)))
Tactic: rw [← isNilpotent_reflect_iff aux, reflect_sub, ← reverse, M.reverse_charpoly]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Disc (hypothesis)
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
⊢ A.discr = HPow.hPow (β := ℕ) A.trace 2 - 4 * A.det
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Disc (goal)
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
⊢ degree A.charpoly = 2
have simp : Eq (α := WithBot ℕ) (↑(Fintype.card n) : WithBot ℕ) 2
Tactic: simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Disc (goal)
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
⊢ A.discr = HPow.hPow (β := ℕ) A.trace 2 - 4 * A.det
have 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
Tactic: rw [discr, Polynomial.discr_of_degree_eq_two (by simp; norm_cast)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs (goal)
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
⊢ B.det = (roots B.charpoly).prod
have rw : HPow.hPow (α := R) (-1) (Fintype.card n) * coeff B.charpoly 0 = (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs (goal)
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
⊢ B.det = (roots B.charpoly).prod
have rw₁ : HPow.hPow (α := R) (-1) (natDegree B.charpoly) * coeff B.charpoly 0 = (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs (goal)
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
⊢ B.det = (roots B.charpoly).prod
have rw₂ : HPow.hPow (α := R) (-1) (natDegree B.charpoly) *
    (HPow.hPow (α := R) (-1) (natDegree B.charpoly) * (roots B.charpoly).prod) =
  (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs (goal)
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
⊢ B.det = (roots B.charpoly).prod
have rw₃ : HPow.hPow (α := R) (-1) (natDegree B.charpoly) * HPow.hPow (α := R) (-1) (natDegree B.charpoly) *
    (roots B.charpoly).prod =
  (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs (goal)
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
⊢ B.det = (roots B.charpoly).prod
have rw₄ : HPow.hPow (β := ℕ) (HPow.hPow (α := R) (-1) (natDegree B.charpoly)) 2 * (roots B.charpoly).prod =
  (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs (goal)
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
⊢ B.det = (roots B.charpoly).prod
have rw₅ : HPow.hPow (α := R) (β := ℕ) (-1) 2 ^ natDegree B.charpoly * (roots B.charpoly).prod = (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs (goal)
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
⊢ B.det = (roots B.charpoly).prod
have rw₆ : HPow.hPow (α := R) 1 (natDegree B.charpoly) * (roots B.charpoly).prod = (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs (goal)
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
⊢ B.det = (roots B.charpoly).prod
have rw₇ : 1 * (roots B.charpoly).prod = (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs (goal)
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
⊢ B.det = (roots B.charpoly).prod
have rw₈ : (roots B.charpoly).prod = (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs (goal)
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
⊢ B.trace = (roots B.charpoly).sum
have inl : ∀ (h : IsEmpty n), B.trace = (roots B.charpoly).sum
Tactic: rcases isEmpty_or_nonempty n with h | _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs (goal)
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
⊢ B.trace = (roots B.charpoly).sum
have inr : Nonempty n → B.trace = (roots B.charpoly).sum
Tactic: rcases isEmpty_or_nonempty n with h | _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs (goal)
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
⊢ B.trace = (roots B.charpoly).sum
have inr : -nextCoeff B.charpoly = (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs (goal)
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
⊢ B.trace = (roots B.charpoly).sum
have inr₁ : nextCoeff B.charpoly = -(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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs (goal)
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
⊢ B.trace = (roots B.charpoly).sum
have inr₂ : nextCoeff B.charpoly = nextCoeff B.charpoly
Tactic: rw [trace_eq_neg_charpoly_nextCoeff, neg_eq_iff_eq_neg,
      ← hAps.nextCoeff_eq_neg_sum_roots_of_monic B.charpoly_monic]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
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
⊢ Eq (α := K[X]) (M ^ Fintype.card K).charpoly M.charpoly
have inl : Nonempty n → Eq (α := K[X]) (M ^ Fintype.card K).charpoly M.charpoly
Tactic: cases (isEmpty_or_nonempty n).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
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
⊢ Eq (α := K[X]) (M ^ Fintype.card K).charpoly M.charpoly
have inr : IsEmpty n → Eq (α := K[X]) (M ^ Fintype.card K).charpoly M.charpoly
Tactic: cases (isEmpty_or_nonempty n).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
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
⊢ Eq (α := K[X]) (M ^ Fintype.card K).charpoly M.charpoly
have inl : ∀ (p : ℕ) (hp : CharP K p), Eq (α := K[X]) (M ^ Fintype.card K).charpoly M.charpoly
Tactic: obtain ⟨p, hp⟩ := CharP.exists K
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
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
⊢ Eq (α := K[X]) (M ^ Fintype.card K).charpoly M.charpoly
have 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
Tactic: rcases FiniteField.card K p with ⟨⟨k, kpos⟩, ⟨hp, hk⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (hypothesis)
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) : ℕ)
⊢ Eq (α := K[X]) (M ^ Fintype.card K).charpoly M.charpoly
have this : Fact (Nat.Prime p)
Tactic: haveI : Fact p.Prime := ⟨hp⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
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)
⊢ Eq (α := K[X]) (M ^ Fintype.card K).charpoly M.charpoly
have inl : Eq (α := K[X]) (M ^ p ^ k).charpoly M.charpoly
Tactic: rw [hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
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)
⊢ Eq (α := K[X]) (M ^ p ^ k).charpoly M.charpoly
have 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)
Tactic: apply (frobenius_inj K[X] p).iterate k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
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)
⊢ 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)
have inl : HPow.hPow (α := K[X]) (M ^ p ^ k).charpoly (p ^ k) = (⇑(frobenius K[X] p) : (a : K[X]) → K[X])^[k] M.charpoly
Tactic: rw [iterate_frobenius (R := K[X])]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
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)
⊢ HPow.hPow (α := K[X]) (M ^ p ^ k).charpoly (p ^ k) = (⇑(frobenius K[X] p) : (a : K[X]) → K[X])^[k] M.charpoly
have 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
Tactic: rw [← hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
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)
⊢ HPow.hPow (α := K[X]) (M ^ Fintype.card K).charpoly (Fintype.card K) =
    (⇑(frobenius K[X] p) : (a : K[X]) → K[X])^[k] M.charpoly
have inl : HPow.hPow (α := K[X]) (M ^ Fintype.card K).charpoly (Fintype.card K) = HPow.hPow (α := K[X]) M.charpoly (p ^ k)
Tactic: rw [iterate_frobenius (R := K[X])]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
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)
⊢ HPow.hPow (α := K[X]) (M ^ Fintype.card K).charpoly (Fintype.card K) = HPow.hPow (α := K[X]) M.charpoly (p ^ k)
have inl : HPow.hPow (α := K[X]) (M ^ Fintype.card K).charpoly (Fintype.card K) = HPow.hPow (α := K[X]) M.charpoly (Fintype.card K)
Tactic: rw [← hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
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)
⊢ 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)
have inl : HPow.hPow (α := K[X]) (M ^ Fintype.card K).charpoly (Fintype.card K) = HPow.hPow (α := K[X]) M.charpoly (Fintype.card K)
Tactic: repeat' rw [iterate_frobenius (R := K[X])]; rw [← hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
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)
⊢ HPow.hPow (α := K[X]) (M ^ Fintype.card K).charpoly (Fintype.card K) =
    HPow.hPow (α := K[X]) M.charpoly (Fintype.card K)
have inl : (expand K (Fintype.card K) : (a : K[X]) → K[X]) (M ^ Fintype.card K).charpoly =
  HPow.hPow (α := K[X]) M.charpoly (Fintype.card K)
Tactic: rw [← FiniteField.expand_card]