[GOAL]
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
i j : n
⊢ natDegree (charmatrix M i j) = if i = j then 1 else 0
[PROOFSTEP]
by_cases i = j
[GOAL]
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
i j : n
⊢ natDegree (charmatrix M i j) = if i = j then 1 else 0
[PROOFSTEP]
by_cases i = j
[GOAL]
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
i j : n
h : i = j
⊢ natDegree (charmatrix M i j) = if i = j then 1 else 0
[PROOFSTEP]
simp [h, ← degree_eq_iff_natDegree_eq_of_pos (Nat.succ_pos 0)]
[GOAL]
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
i j : n
h : ¬i = j
⊢ natDegree (charmatrix M i j) = if i = j then 1 else 0
[PROOFSTEP]
simp [h, ← degree_eq_iff_natDegree_eq_of_pos (Nat.succ_pos 0)]
[GOAL]
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
i j : n
⊢ natDegree (charmatrix M i j) ≤ if i = j then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
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
i j : n
h : i = j
⊢ natDegree (charmatrix M i j) ≤ 1
[PROOFSTEP]
simp [h, natDegree_X_sub_C_le]
[GOAL]
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
i j : n
h : ¬i = j
⊢ natDegree (charmatrix M i j) ≤ 0
[PROOFSTEP]
simp [h, natDegree_X_sub_C_le]
[GOAL]
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
⊢ degree (charpoly M - ∏ i : n, (X - ↑C (M i i))) < ↑(Fintype.card n - 1)
[PROOFSTEP]
rw [charpoly, det_apply', ← insert_erase (mem_univ (Equiv.refl n)), sum_insert (not_mem_erase (Equiv.refl n) univ),
  add_comm]
[GOAL]
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
⊢ degree
      (∑ x in Finset.erase univ (Equiv.refl n), ↑↑(↑Equiv.Perm.sign x) * ∏ i : n, charmatrix M (↑x i) i +
          ↑↑(↑Equiv.Perm.sign (Equiv.refl n)) * ∏ i : n, charmatrix M (↑(Equiv.refl n) i) i -
        ∏ i : n, (X - ↑C (M i i))) <
    ↑(Fintype.card n - 1)
[PROOFSTEP]
simp only [charmatrix_apply_eq, one_mul, Equiv.Perm.sign_refl, id.def, Int.cast_one, Units.val_one, add_sub_cancel,
  Equiv.coe_refl]
[GOAL]
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
⊢ degree (∑ x in Finset.erase univ (Equiv.refl n), ↑↑(↑Equiv.Perm.sign x) * ∏ x_1 : n, charmatrix M (↑x x_1) x_1) <
    ↑(Fintype.card n - 1)
[PROOFSTEP]
rw [← mem_degreeLT]
[GOAL]
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
⊢ ∑ x in Finset.erase univ (Equiv.refl n), ↑↑(↑Equiv.Perm.sign x) * ∏ x_1 : n, charmatrix M (↑x x_1) x_1 ∈
    degreeLT R (Fintype.card n - 1)
[PROOFSTEP]
apply Submodule.sum_mem (degreeLT R (Fintype.card n - 1))
[GOAL]
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
⊢ ∀ (c : n ≃ n),
    c ∈ Finset.erase univ (Equiv.refl n) →
      ↑↑(↑Equiv.Perm.sign c) * ∏ x : n, charmatrix M (↑c x) x ∈ degreeLT R (Fintype.card n - 1)
[PROOFSTEP]
intro c hc
[GOAL]
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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ ↑↑(↑Equiv.Perm.sign c) * ∏ x : n, charmatrix M (↑c x) x ∈ degreeLT R (Fintype.card n - 1)
[PROOFSTEP]
rw [← C_eq_int_cast, C_mul']
[GOAL]
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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ ↑↑(↑Equiv.Perm.sign c) • ∏ x : n, charmatrix M (↑c x) x ∈ degreeLT R (Fintype.card n - 1)
[PROOFSTEP]
apply Submodule.smul_mem (degreeLT R (Fintype.card n - 1)) ↑↑(Equiv.Perm.sign c)
[GOAL]
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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ ∏ x : n, charmatrix M (↑c x) x ∈ degreeLT R (Fintype.card n - 1)
[PROOFSTEP]
rw [mem_degreeLT]
[GOAL]
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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ degree (∏ x : n, charmatrix M (↑c x) x) < ↑(Fintype.card n - 1)
[PROOFSTEP]
apply lt_of_le_of_lt degree_le_natDegree _
[GOAL]
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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ ↑(natDegree (∏ x : n, charmatrix M (↑c x) x)) < ↑(Fintype.card n - 1)
[PROOFSTEP]
rw [Nat.cast_withBot, Nat.cast_withBot]
  -- porting note: added
[GOAL]
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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ ↑(natDegree (∏ x : n, charmatrix M (↑c x) x)) < ↑(Fintype.card n - 1)
[PROOFSTEP]
rw [WithBot.coe_lt_coe]
[GOAL]
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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ natDegree (∏ x : n, charmatrix M (↑c x) x) < Fintype.card n - 1
[PROOFSTEP]
apply lt_of_le_of_lt _ (Equiv.Perm.fixed_point_card_lt_of_ne_one (ne_of_mem_erase hc))
[GOAL]
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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ natDegree (∏ x : n, charmatrix M (↑c x) x) ≤ card (filter (fun x => ↑c x = x) univ)
[PROOFSTEP]
apply le_trans (Polynomial.natDegree_prod_le univ fun i : n => charmatrix M (c i) i) _
[GOAL]
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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ ∑ i : n, natDegree (charmatrix M (↑c i) i) ≤ card (filter (fun x => ↑c x = x) univ)
[PROOFSTEP]
rw [card_eq_sum_ones]
[GOAL]
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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ ∑ i : n, natDegree (charmatrix M (↑c i) i) ≤ ∑ x in filter (fun x => ↑c x = x) univ, 1
[PROOFSTEP]
rw [sum_filter]
[GOAL]
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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ ∑ i : n, natDegree (charmatrix M (↑c i) i) ≤ ∑ a : n, if ↑c a = a then 1 else 0
[PROOFSTEP]
apply sum_le_sum
[GOAL]
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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ ∀ (i : n), i ∈ univ → natDegree (charmatrix M (↑c i) i) ≤ if ↑c i = i then 1 else 0
[PROOFSTEP]
intros
[GOAL]
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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
i✝ : n
a✝ : i✝ ∈ univ
⊢ natDegree (charmatrix M (↑c i✝) i✝) ≤ if ↑c i✝ = i✝ then 1 else 0
[PROOFSTEP]
apply charmatrix_apply_natDegree_le
[GOAL]
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
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ coeff (charpoly M) k = coeff (∏ i : n, (X - ↑C (M i i))) k
[PROOFSTEP]
apply eq_of_sub_eq_zero
[GOAL]
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
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ coeff (charpoly M) k - coeff (∏ i : n, (X - ↑C (M i i))) k = 0
[PROOFSTEP]
rw [← coeff_sub]
[GOAL]
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
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ coeff (charpoly M - ∏ i : n, (X - ↑C (M i i))) k = 0
[PROOFSTEP]
apply Polynomial.coeff_eq_zero_of_degree_lt
[GOAL]
case h.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
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ degree (charpoly M - ∏ i : n, (X - ↑C (M i i))) < ↑k
[PROOFSTEP]
apply lt_of_lt_of_le (charpoly_sub_diagonal_degree_lt M) ?_
[GOAL]
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
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ ↑(Fintype.card n - 1) ≤ ↑k
[PROOFSTEP]
rw [Nat.cast_withBot, Nat.cast_withBot]
  -- porting note: added
[GOAL]
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
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ ↑(Fintype.card n - 1) ≤ ↑k
[PROOFSTEP]
rw [WithBot.coe_le_coe]
[GOAL]
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
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ Fintype.card n - 1 ≤ k
[PROOFSTEP]
apply h
[GOAL]
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
h : Fintype.card n = 0
M : Matrix n n R
⊢ det M = 1
[PROOFSTEP]
rw [Fintype.card_eq_zero_iff] at h 
[GOAL]
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
h : IsEmpty n
M : Matrix n n R
⊢ det M = 1
[PROOFSTEP]
suffices M = 1 by simp [this]
[GOAL]
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
h : IsEmpty n
M : Matrix n n R
this : M = 1
⊢ det M = 1
[PROOFSTEP]
simp [this]
[GOAL]
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
h : IsEmpty n
M : Matrix n n R
⊢ M = 1
[PROOFSTEP]
ext i
[GOAL]
case a.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
h : IsEmpty n
M : Matrix n n R
i x✝ : n
⊢ M i x✝ = OfNat.ofNat 1 i x✝
[PROOFSTEP]
exact h.elim i
[GOAL]
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)
[PROOFSTEP]
by_cases h : Fintype.card n = 0
[GOAL]
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)
[PROOFSTEP]
rw [h]
[GOAL]
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
[PROOFSTEP]
unfold charpoly
[GOAL]
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
[PROOFSTEP]
rw [det_of_card_zero]
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
assumption
[GOAL]
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)
[PROOFSTEP]
rw [← sub_add_cancel M.charpoly (∏ i : n, (X - C (M i i)))]
  -- porting note: added `↑` in front of `Fintype.card n`
[GOAL]
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)
[PROOFSTEP]
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
[GOAL]
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)
[PROOFSTEP]
rw [degree_eq_iff_natDegree_eq_of_pos (Nat.pos_of_ne_zero h), natDegree_prod']
[GOAL]
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
[PROOFSTEP]
simp_rw [natDegree_X_sub_C]
[GOAL]
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
[PROOFSTEP]
rw [← Finset.card_univ, sum_const, smul_eq_mul, mul_one]
[GOAL]
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
[PROOFSTEP]
simp_rw [(monic_X_sub_C _).leadingCoeff]
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
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)
[PROOFSTEP]
rw [degree_add_eq_right_of_degree_lt]
[GOAL]
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)))
[PROOFSTEP]
exact h1
[GOAL]
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)))
[PROOFSTEP]
rw [h1]
[GOAL]
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)
[PROOFSTEP]
apply lt_trans (charpoly_sub_diagonal_degree_lt M)
[GOAL]
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)
[PROOFSTEP]
rw [Nat.cast_withBot, Nat.cast_withBot]
  -- porting note: added
[GOAL]
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)
[PROOFSTEP]
rw [WithBot.coe_lt_coe]
[GOAL]
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
[PROOFSTEP]
rw [← Nat.pred_eq_sub_one]
[GOAL]
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
[PROOFSTEP]
apply Nat.pred_lt
[GOAL]
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
[PROOFSTEP]
apply h
[GOAL]
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)
[PROOFSTEP]
nontriviality R
[GOAL]
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)
[PROOFSTEP]
by_cases h : Fintype.card n = 0
[GOAL]
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)
[PROOFSTEP]
rw [charpoly, det_of_card_zero h]
[GOAL]
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
[PROOFSTEP]
apply monic_one
[GOAL]
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)
[PROOFSTEP]
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]
[GOAL]
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)))
[PROOFSTEP]
apply monic_prod_of_monic univ fun i : n => X - C (M i i)
[GOAL]
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))
[PROOFSTEP]
simp [monic_X_sub_C]
[GOAL]
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)
[PROOFSTEP]
rw [← sub_add_cancel (∏ i : n, (X - C (M i i))) M.charpoly] at mon 
[GOAL]
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)
[PROOFSTEP]
rw [Monic] at *
[GOAL]
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
[PROOFSTEP]
rwa [leadingCoeff_add_of_degree_lt] at mon 
[GOAL]
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)
[PROOFSTEP]
rw [charpoly_degree_eq_dim]
[GOAL]
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)
[PROOFSTEP]
rw [← neg_sub]
[GOAL]
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)
[PROOFSTEP]
rw [degree_neg]
[GOAL]
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)
[PROOFSTEP]
apply lt_trans (charpoly_sub_diagonal_degree_lt M)
[GOAL]
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)
[PROOFSTEP]
rw [Nat.cast_withBot, Nat.cast_withBot]
  -- porting note: added
[GOAL]
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)
[PROOFSTEP]
rw [WithBot.coe_lt_coe]
[GOAL]
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
[PROOFSTEP]
rw [← Nat.pred_eq_sub_one]
[GOAL]
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
[PROOFSTEP]
apply Nat.pred_lt
[GOAL]
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
[PROOFSTEP]
apply h
[GOAL]
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✝ : Nonempty n
M : Matrix n n R
⊢ trace M = -coeff (charpoly M) (Fintype.card n - 1)
[PROOFSTEP]
rw [charpoly_coeff_eq_prod_coeff_of_le _ le_rfl, Fintype.card,
  prod_X_sub_C_coeff_card_pred univ (fun i : n => M i i) Fintype.card_pos, neg_neg, trace]
[GOAL]
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✝ : Nonempty n
M : Matrix n n R
⊢ ∑ i : n, diag M i = ∑ i : n, M i i
[PROOFSTEP]
simp_rw [diag_apply]
[GOAL]
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
M : Matrix n n R[X]
r : R
i j : n
⊢ eval (↑(scalar n) r) (↑matPolyEquiv M) i j = eval r (M i j)
[PROOFSTEP]
unfold Polynomial.eval
[GOAL]
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
M : Matrix n n R[X]
r : R
i j : n
⊢ eval₂ (RingHom.id ((fun x => Matrix n n R) r)) (↑(scalar n) r) (↑matPolyEquiv M) i j = eval₂ (RingHom.id R) r (M i j)
[PROOFSTEP]
rw [Polynomial.eval₂_def, Polynomial.eval₂_def]
  -- porting note: was `unfold eval₂`
[GOAL]
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
M : Matrix n n R[X]
r : R
i j : n
⊢ sum (↑matPolyEquiv M) (fun e a => ↑(RingHom.id ((fun x => Matrix n n R) r)) a * ↑(scalar n) r ^ e) i j =
    sum (M i j) fun e a => ↑(RingHom.id R) a * r ^ e
[PROOFSTEP]
trans Polynomial.sum (matPolyEquiv M) fun (e : ℕ) (a : Matrix n n R) => (a * (scalar n) r ^ e) i j
[GOAL]
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
M : Matrix n n R[X]
r : R
i j : n
⊢ sum (↑matPolyEquiv M) (fun e a => ↑(RingHom.id ((fun x => Matrix n n R) r)) a * ↑(scalar n) r ^ e) i j =
    sum (↑matPolyEquiv M) fun e a => (a * ↑(scalar n) r ^ e) i j
[PROOFSTEP]
unfold Polynomial.sum
[GOAL]
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
M : Matrix n n R[X]
r : R
i j : n
⊢ Finset.sum (support (↑matPolyEquiv M))
      (fun n_1 =>
        (fun e a => ↑(RingHom.id ((fun x => Matrix n n R) r)) a * ↑(scalar n) r ^ e) n_1 (coeff (↑matPolyEquiv M) n_1))
      i j =
    ∑ n_1 in support (↑matPolyEquiv M), (fun e a => (a * ↑(scalar n) r ^ e) i j) n_1 (coeff (↑matPolyEquiv M) n_1)
[PROOFSTEP]
simp only [sum_apply]
[GOAL]
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
M : Matrix n n R[X]
r : R
i j : n
⊢ ∑ c in support (↑matPolyEquiv M), (↑(RingHom.id (Matrix n n R)) (coeff (↑matPolyEquiv M) c) * ↑(scalar n) r ^ c) i j =
    ∑ x in support (↑matPolyEquiv M), (coeff (↑matPolyEquiv M) x * ↑(scalar n) r ^ x) i j
[PROOFSTEP]
dsimp
[GOAL]
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
M : Matrix n n R[X]
r : R
i j : n
⊢ (sum (↑matPolyEquiv M) fun e a => (a * ↑(scalar n) r ^ e) i j) = sum (M i j) fun e a => ↑(RingHom.id R) a * r ^ e
[PROOFSTEP]
simp_rw [← RingHom.map_pow, ← (scalar.commute _ _).eq]
[GOAL]
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
M : Matrix n n R[X]
r : R
i j : n
⊢ (sum (↑matPolyEquiv M) fun e a => (↑(scalar n) (r ^ e) * a) i j) = sum (M i j) fun e a => ↑(RingHom.id R) a * r ^ e
[PROOFSTEP]
simp only [coe_scalar, Matrix.one_mul, RingHom.id_apply, Pi.smul_apply, smul_eq_mul, Algebra.smul_mul_assoc]
  -- porting note: the `have` was present and unused also in the original
      --have h : ∀ x : ℕ, (fun (e : ℕ) (a : R) => r ^ e * a) x 0 = 0 := by simp
[GOAL]
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
M : Matrix n n R[X]
r : R
i j : n
⊢ (sum (↑matPolyEquiv M) fun e a => (r ^ e • a) i j) = sum (M i j) fun e a => a * r ^ e
[PROOFSTEP]
simp only [Polynomial.sum, matPolyEquiv_coeff_apply, mul_comm]
[GOAL]
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
M : Matrix n n R[X]
r : R
i j : n
⊢ ∑ x in support (↑matPolyEquiv M), (r ^ x • coeff (↑matPolyEquiv M) x) i j =
    ∑ x in support (M i j), r ^ x * coeff (M i j) x
[PROOFSTEP]
simp only [smul_apply, matPolyEquiv_coeff_apply, smul_eq_mul]
  -- porting note: added
[GOAL]
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
M : Matrix n n R[X]
r : R
i j : n
⊢ ∑ x in support (↑matPolyEquiv M), r ^ x * coeff (M i j) x = ∑ x in support (M i j), r ^ x * coeff (M i j) x
[PROOFSTEP]
apply (Finset.sum_subset (support_subset_support_matPolyEquiv _ _ _) _).symm
[GOAL]
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
M : Matrix n n R[X]
r : R
i j : n
⊢ ∀ (x : ℕ), x ∈ support (↑matPolyEquiv M) → ¬x ∈ support (M i j) → r ^ x * coeff (M i j) x = 0
[PROOFSTEP]
intro n _hn h'n
[GOAL]
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
M : Matrix n✝ n✝ R[X]
r : R
i j : n✝
n : ℕ
_hn : n ∈ support (↑matPolyEquiv M)
h'n : ¬n ∈ support (M i j)
⊢ r ^ n * coeff (M i j) n = 0
[PROOFSTEP]
rw [not_mem_support_iff] at h'n 
[GOAL]
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
M : Matrix n✝ n✝ R[X]
r : R
i j : n✝
n : ℕ
_hn : n ∈ support (↑matPolyEquiv M)
h'n : coeff (M i j) n = 0
⊢ r ^ n * coeff (M i j) n = 0
[PROOFSTEP]
simp only [h'n, zero_mul]
[GOAL]
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
M : Matrix n✝ n✝ R[X]
r : R
i j : n✝
n : ℕ
_hn : n ∈ support (↑matPolyEquiv M)
h'n : coeff (M i j) n = 0
⊢ r ^ n * 0 = 0
[PROOFSTEP]
simp only [mul_zero]
  -- porting note: added
[GOAL]
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
M : Matrix n n R[X]
r : R
⊢ eval r (det M) = det (eval (↑(scalar n) r) (↑matPolyEquiv M))
[PROOFSTEP]
rw [Polynomial.eval, ← coe_eval₂RingHom, RingHom.map_det]
[GOAL]
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
M : Matrix n n R[X]
r : R
⊢ det (↑(RingHom.mapMatrix (eval₂RingHom (RingHom.id R) r)) M) = det (eval (↑(scalar n) r) (↑matPolyEquiv M))
[PROOFSTEP]
apply congr_arg det
[GOAL]
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
M : Matrix n n R[X]
r : R
⊢ ↑(RingHom.mapMatrix (eval₂RingHom (RingHom.id R) r)) M = eval (↑(scalar n) r) (↑matPolyEquiv M)
[PROOFSTEP]
ext
[GOAL]
case a.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
M : Matrix n n R[X]
r : R
i✝ x✝ : n
⊢ ↑(RingHom.mapMatrix (eval₂RingHom (RingHom.id R) r)) M i✝ x✝ = eval (↑(scalar n) r) (↑matPolyEquiv M) i✝ x✝
[PROOFSTEP]
symm
  -- porting note: `exact` was `convert`
[GOAL]
case a.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
M : Matrix n n R[X]
r : R
i✝ x✝ : n
⊢ eval (↑(scalar n) r) (↑matPolyEquiv M) i✝ x✝ = ↑(RingHom.mapMatrix (eval₂RingHom (RingHom.id R) r)) M i✝ x✝
[PROOFSTEP]
exact matPolyEquiv_eval _ _ _ _
[GOAL]
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
⊢ det M = (-1) ^ Fintype.card n * coeff (charpoly M) 0
[PROOFSTEP]
rw [coeff_zero_eq_eval_zero, charpoly, eval_det, matPolyEquiv_charmatrix, ← det_smul]
[GOAL]
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
⊢ det M = det (-1 • eval (↑(scalar n) 0) (X - ↑C M))
[PROOFSTEP]
simp
[GOAL]
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
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
⊢ ↑matPolyEquiv (↑(RingHom.mapMatrix ↑(expand K k)) (charmatrix (M ^ k))) = X ^ k - ↑C (M ^ k)
[PROOFSTEP]
ext m i j
[GOAL]
case a.a.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
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
⊢ coeff (↑matPolyEquiv (↑(RingHom.mapMatrix ↑(expand K k)) (charmatrix (M ^ k)))) m i j =
    coeff (X ^ k - ↑C (M ^ k)) m i j
[PROOFSTEP]
rw [coeff_sub, coeff_C, matPolyEquiv_coeff_apply, RingHom.mapMatrix_apply, Matrix.map_apply, AlgHom.coe_toRingHom,
  DMatrix.sub_apply, coeff_X_pow]
[GOAL]
case a.a.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
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
⊢ coeff (↑(expand K k) (charmatrix (M ^ k) i j)) m = ite (m = k) 1 0 i j - ite (m = 0) (M ^ k) 0 i j
[PROOFSTEP]
by_cases hij : i = j
[GOAL]
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
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
⊢ coeff (↑(expand K k) (charmatrix (M ^ k) i j)) m = ite (m = k) 1 0 i j - ite (m = 0) (M ^ k) 0 i j
[PROOFSTEP]
rw [hij, charmatrix_apply_eq, AlgHom.map_sub, expand_C, expand_X, coeff_sub, coeff_X_pow, coeff_C]
  -- porting note: the second `Matrix.` was `DMatrix.`
[GOAL]
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
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
⊢ ((if m = k then 1 else 0) - if m = 0 then (M ^ k) j j else 0) = ite (m = k) 1 0 j j - ite (m = 0) (M ^ k) 0 j j
[PROOFSTEP]
split_ifs with mp m0
[GOAL]
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
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : m = k
m0 : m = 0
⊢ 1 - (M ^ k) j j = OfNat.ofNat 1 j j - (M ^ k) j j
[PROOFSTEP]
simp only [Matrix.one_apply_eq, Matrix.zero_apply]
[GOAL]
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
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : m = k
m0 : ¬m = 0
⊢ 1 - 0 = OfNat.ofNat 1 j j - OfNat.ofNat 0 j j
[PROOFSTEP]
simp only [Matrix.one_apply_eq, Matrix.zero_apply]
[GOAL]
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
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : ¬m = k
h✝ : m = 0
⊢ 0 - (M ^ k) j j = OfNat.ofNat 0 j j - (M ^ k) j j
[PROOFSTEP]
simp only [Matrix.one_apply_eq, Matrix.zero_apply]
[GOAL]
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
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : ¬m = k
h✝ : ¬m = 0
⊢ 0 - 0 = OfNat.ofNat 0 j j - OfNat.ofNat 0 j j
[PROOFSTEP]
simp only [Matrix.one_apply_eq, Matrix.zero_apply]
[GOAL]
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
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
⊢ coeff (↑(expand K k) (charmatrix (M ^ k) i j)) m = ite (m = k) 1 0 i j - ite (m = 0) (M ^ k) 0 i j
[PROOFSTEP]
rw [charmatrix_apply_ne _ _ _ hij, AlgHom.map_neg, expand_C, coeff_neg, coeff_C]
[GOAL]
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
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
⊢ (-if m = 0 then (M ^ k) i j else 0) = ite (m = k) 1 0 i j - ite (m = 0) (M ^ k) 0 i j
[PROOFSTEP]
split_ifs with m0 mp
[GOAL]
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
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
m0 : m = 0
mp : m = k
⊢ -(M ^ k) i j = OfNat.ofNat 1 i j - (M ^ k) i j
[PROOFSTEP]
simp only [hij, zero_sub, Matrix.zero_apply, sub_zero, neg_zero, Matrix.one_apply_ne, Ne.def, not_false_iff]
[GOAL]
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
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
m0 : m = 0
mp : ¬m = k
⊢ -(M ^ k) i j = OfNat.ofNat 0 i j - (M ^ k) i j
[PROOFSTEP]
simp only [hij, zero_sub, Matrix.zero_apply, sub_zero, neg_zero, Matrix.one_apply_ne, Ne.def, not_false_iff]
[GOAL]
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
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
m0 : ¬m = 0
h✝ : m = k
⊢ -0 = OfNat.ofNat 1 i j - OfNat.ofNat 0 i j
[PROOFSTEP]
simp only [hij, zero_sub, Matrix.zero_apply, sub_zero, neg_zero, Matrix.one_apply_ne, Ne.def, not_false_iff]
[GOAL]
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
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
m0 : ¬m = 0
h✝ : ¬m = k
⊢ -0 = OfNat.ofNat 0 i j - OfNat.ofNat 0 i j
[PROOFSTEP]
simp only [hij, zero_sub, Matrix.zero_apply, sub_zero, neg_zero, Matrix.one_apply_ne, Ne.def, not_false_iff]
[GOAL]
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
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n R
k : ℕ
⊢ M ^ k = ↑(aeval M) (X ^ k %ₘ charpoly M)
[PROOFSTEP]
rw [← aeval_eq_aeval_mod_charpoly, map_pow, aeval_X]
[GOAL]
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
p : ℕ
inst✝ : Fact (Nat.Prime p)
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
⊢ coeff (charpoly M) k ∈ I ^ (Fintype.card n - k)
[PROOFSTEP]
delta charpoly
[GOAL]
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
p : ℕ
inst✝ : Fact (Nat.Prime p)
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
⊢ coeff (det (charmatrix M)) k ∈ I ^ (Fintype.card n - k)
[PROOFSTEP]
rw [Matrix.det_apply, finset_sum_coeff]
[GOAL]
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
p : ℕ
inst✝ : Fact (Nat.Prime p)
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
⊢ ∑ b : Equiv.Perm n, coeff (↑Equiv.Perm.sign b • ∏ i : n, charmatrix M (↑b i) i) k ∈ I ^ (Fintype.card n - k)
[PROOFSTEP]
apply sum_mem
[GOAL]
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
p : ℕ
inst✝ : Fact (Nat.Prime p)
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
⊢ ∀ (c : Equiv.Perm n),
    c ∈ univ → coeff (↑Equiv.Perm.sign c • ∏ i : n, charmatrix M (↑c i) i) k ∈ I ^ (Fintype.card n - k)
[PROOFSTEP]
rintro c -
[GOAL]
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
p : ℕ
inst✝ : Fact (Nat.Prime p)
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
⊢ coeff (↑Equiv.Perm.sign c • ∏ i : n, charmatrix M (↑c i) i) k ∈ I ^ (Fintype.card n - k)
[PROOFSTEP]
rw [coeff_smul, Submodule.smul_mem_iff']
[GOAL]
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
p : ℕ
inst✝ : Fact (Nat.Prime p)
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
⊢ coeff (∏ i : n, charmatrix M (↑c i) i) k ∈ I ^ (Fintype.card n - k)
[PROOFSTEP]
have : ∑ x : n, 1 = Fintype.card n := by rw [Finset.sum_const, card_univ, smul_eq_mul, mul_one]
[GOAL]
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
p : ℕ
inst✝ : Fact (Nat.Prime p)
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
⊢ ∑ x : n, 1 = Fintype.card n
[PROOFSTEP]
rw [Finset.sum_const, card_univ, smul_eq_mul, mul_one]
[GOAL]
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
p : ℕ
inst✝ : Fact (Nat.Prime p)
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
⊢ coeff (∏ i : n, charmatrix M (↑c i) i) k ∈ I ^ (Fintype.card n - k)
[PROOFSTEP]
rw [← this]
[GOAL]
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
p : ℕ
inst✝ : Fact (Nat.Prime p)
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
⊢ coeff (∏ i : n, charmatrix M (↑c i) i) k ∈ I ^ (∑ x : n, 1 - k)
[PROOFSTEP]
apply coeff_prod_mem_ideal_pow_tsub
[GOAL]
case h.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
p : ℕ
inst✝ : Fact (Nat.Prime p)
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
⊢ ∀ (i : n), i ∈ univ → ∀ (k : ℕ), coeff (charmatrix M (↑c i) i) k ∈ I ^ (1 - k)
[PROOFSTEP]
rintro i - (_ | k)
[GOAL]
case h.h.zero
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
p : ℕ
inst✝ : Fact (Nat.Prime p)
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
i : n
⊢ coeff (charmatrix M (↑c i) i) Nat.zero ∈ I ^ (1 - Nat.zero)
[PROOFSTEP]
rw [Nat.zero_eq]
  -- porting note: `rw [Nat.zero_eq]` was not present
[GOAL]
case h.h.zero
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
p : ℕ
inst✝ : Fact (Nat.Prime p)
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
i : n
⊢ coeff (charmatrix M (↑c i) i) 0 ∈ I ^ (1 - 0)
[PROOFSTEP]
rw [tsub_zero, pow_one, charmatrix_apply, coeff_sub, coeff_X_mul_zero, coeff_C_zero, zero_sub]
[GOAL]
case h.h.zero
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
p : ℕ
inst✝ : Fact (Nat.Prime p)
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
i : n
⊢ -M (↑c i) i ∈ I
[PROOFSTEP]
apply neg_mem
[GOAL]
case h.h.zero.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
p : ℕ
inst✝ : Fact (Nat.Prime p)
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
i : n
⊢ M (↑c i) i ∈ I
[PROOFSTEP]
exact h (c i) i
[GOAL]
case h.h.succ
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
p : ℕ
inst✝ : Fact (Nat.Prime p)
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k✝ : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
i : n
k : ℕ
⊢ coeff (charmatrix M (↑c i) i) (Nat.succ k) ∈ I ^ (1 - Nat.succ k)
[PROOFSTEP]
rw [Nat.succ_eq_one_add, tsub_self_add, pow_zero, Ideal.one_eq_top]
[GOAL]
case h.h.succ
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
p : ℕ
inst✝ : Fact (Nat.Prime p)
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k✝ : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
i : n
k : ℕ
⊢ coeff (charmatrix M (↑c i) i) (1 + k) ∈ ⊤
[PROOFSTEP]
exact Submodule.mem_top
