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

case neg
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
⊢ Monic (charpoly M)
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
✝ : Nontrivial R
⊢ Monic (charpoly M)
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✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : Monic (∏ i : n, (X - ↑C (M i i)))
⊢ Monic (charpoly M)
case neg
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
⊢ Monic (charpoly M)
have mon : (∏ i : n, (X - C (M i i))).Monic := by
  apply monic_prod_of_monic univ fun i : n => X - C (M i i)
  simp [monic_X_sub_C]
case neg
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : Monic (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M)
⊢ Monic (charpoly M)
case neg
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : Monic (∏ i : n, (X - ↑C (M i i)))
⊢ Monic (charpoly M)
rw [← sub_add_cancel (∏ i : n, (X - C (M i i))) M.charpoly] at mon
case neg
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ leadingCoeff (charpoly M) = 1
case neg
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : Monic (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M)
⊢ Monic (charpoly M)
rw [Monic] at *
case neg
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ degree (∏ i : n, (X - ↑C (M i i)) - charpoly M) < degree (charpoly M)
case neg
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ leadingCoeff (charpoly M) = 1
rwa [leadingCoeff_add_of_degree_lt] at mon
case neg
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ degree (∏ i : n, (X - ↑C (M i i)) - 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✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ degree (∏ i : n, (X - ↑C (M i i)) - charpoly M) < degree (charpoly M)
rw [charpoly_degree_eq_dim]
case neg
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ 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✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ degree (∏ i : n, (X - ↑C (M i i)) - charpoly M) < ↑(Fintype.card n)
rw [← neg_sub]
case neg
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ 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✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ degree (-(charpoly M - ∏ i : n, (X - ↑C (M i i)))) < ↑(Fintype.card n)
rw [degree_neg]
case neg
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ ↑(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✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ 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✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ ↑(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✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ ↑(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✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ 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✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ ↑(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✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ 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✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ 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✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ 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✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ 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✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : leadingCoeff (∏ i : n, (X - ↑C (M i i)) - charpoly M + charpoly M) = 1
⊢ 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✝ M : Matrix n n R
✝ : Nontrivial R
h : Fintype.card n = 0
⊢ Monic 1
case pos
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
✝ : Nontrivial R
h : Fintype.card n = 0
⊢ Monic (charpoly M)
rw [charpoly, det_of_card_zero h]
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✝ M : Matrix n n R
✝ : Nontrivial R
h : Fintype.card n = 0
⊢ Monic 1
apply monic_one
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
⊢ ∀ (i : n), i ∈ univ → Monic (X - ↑C (M i i))
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
⊢ Monic (∏ i : n, (X - ↑C (M i i)))
apply monic_prod_of_monic univ fun i : n => X - C (M i i)
no goals
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
✝ : Nontrivial R
h : ¬Fintype.card n = 0
⊢ ∀ (i : n), i ∈ univ → Monic (X - ↑C (M i i))
simp [monic_X_sub_C]