case pos
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ degree (charpoly M) = ↑(Fintype.card n)

case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ degree (charpoly M) = ↑(Fintype.card n)
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
⊢ degree (charpoly M) = ↑(Fintype.card n)
by_cases h : Fintype.card n = 0
case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ degree (charpoly M - ∏ i : n, (X - ↑C (M i i)) + ∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ degree (charpoly M) = ↑(Fintype.card n)
rw [← sub_add_cancel M.charpoly (∏ i : n, (X - C (M i i)))]
case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ degree (charpoly M - ∏ i : n, (X - ↑C (M i i)) + ∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ degree (charpoly M - ∏ i : n, (X - ↑C (M i i)) + ∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
have h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n) := by
  rw [degree_eq_iff_natDegree_eq_of_pos (Nat.pos_of_ne_zero h), natDegree_prod']
  simp_rw [natDegree_X_sub_C]
  rw [← Finset.card_univ, sum_const, smul_eq_mul, mul_one]
  simp_rw [(monic_X_sub_C _).leadingCoeff]
  simp
case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)

case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ degree (charpoly M - ∏ i : n, (X - ↑C (M i i))) < degree (∏ i : n, (X - ↑C (M i i)))
case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ degree (charpoly M - ∏ i : n, (X - ↑C (M i i)) + ∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
rw [degree_add_eq_right_of_degree_lt]
case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ degree (charpoly M - ∏ i : n, (X - ↑C (M i i))) < degree (∏ i : n, (X - ↑C (M i i)))
case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)

case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ degree (charpoly M - ∏ i : n, (X - ↑C (M i i))) < degree (∏ i : n, (X - ↑C (M i i)))
exact h1
case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ degree (charpoly M - ∏ i : n, (X - ↑C (M i i))) < ↑(Fintype.card n)
case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ degree (charpoly M - ∏ i : n, (X - ↑C (M i i))) < degree (∏ i : n, (X - ↑C (M i i)))
rw [h1]
case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ ↑(Fintype.card n - 1) < ↑(Fintype.card n)
case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ degree (charpoly M - ∏ i : n, (X - ↑C (M i i))) < ↑(Fintype.card n)
apply lt_trans (charpoly_sub_diagonal_degree_lt M)
case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ ↑(Fintype.card n - 1) < ↑(Fintype.card n)
case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ ↑(Fintype.card n - 1) < ↑(Fintype.card n)
rw [Nat.cast_withBot, Nat.cast_withBot]
case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ Fintype.card n - 1 < Fintype.card n
case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ ↑(Fintype.card n - 1) < ↑(Fintype.card n)
rw [WithBot.coe_lt_coe]
case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ Nat.pred (Fintype.card n) < Fintype.card n
case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ Fintype.card n - 1 < Fintype.card n
rw [← Nat.pred_eq_sub_one]
case neg.a
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ Fintype.card n ≠ 0
case neg
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ Nat.pred (Fintype.card n) < Fintype.card n
apply Nat.pred_lt
no goals
case neg.a
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
⊢ Fintype.card n ≠ 0
apply h
case pos
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ degree (charpoly M) = ↑0
case pos
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ degree (charpoly M) = ↑(Fintype.card n)
rw [h]
case pos
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ degree (det (charmatrix M)) = ↑0
case pos
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ degree (charpoly M) = ↑0
unfold charpoly
case pos
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ degree 1 = ↑0

case pos.h
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ Fintype.card n = 0
case pos
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ degree (det (charmatrix M)) = ↑0
rw [det_of_card_zero]
no goals
case pos
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ degree 1 = ↑0
simp
no goals
case pos.h
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ Fintype.card n = 0
assumption
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∑ i : n, natDegree (X - ↑C (M i i)) = Fintype.card n

case h
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∏ i : n, leadingCoeff (X - ↑C (M i i)) ≠ 0
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ degree (∏ i : n, (X - ↑C (M i i))) = ↑(Fintype.card n)
rw [degree_eq_iff_natDegree_eq_of_pos (Nat.pos_of_ne_zero h), natDegree_prod']
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∑ x : n, 1 = Fintype.card n

case h
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∏ i : n, leadingCoeff (X - ↑C (M i i)) ≠ 0
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∑ i : n, natDegree (X - ↑C (M i i)) = Fintype.card n

case h
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∏ i : n, leadingCoeff (X - ↑C (M i i)) ≠ 0
simp_rw [natDegree_X_sub_C]
case h
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∏ i : n, leadingCoeff (X - ↑C (M i i)) ≠ 0
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∑ x : n, 1 = Fintype.card n

case h
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∏ i : n, leadingCoeff (X - ↑C (M i i)) ≠ 0
rw [← Finset.card_univ, sum_const, smul_eq_mul, mul_one]
case h
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∏ x : n, 1 ≠ 0
case h
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∏ i : n, leadingCoeff (X - ↑C (M i i)) ≠ 0
simp_rw [(monic_X_sub_C _).leadingCoeff]
no goals
case h
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∏ x : n, 1 ≠ 0
simp