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)
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)
rw [charpoly, det_apply', ← insert_erase (mem_univ (Equiv.refl n)),
  sum_insert (not_mem_erase (Equiv.refl n) univ), add_comm]
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)
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)
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]
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)
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)
rw [← mem_degreeLT]
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)
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)
apply Submodule.sum_mem (degreeLT R (Fintype.card n - 1))
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)
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)
intro c hc
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)
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)
rw [← C_eq_int_cast, C_mul']
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)
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)
apply Submodule.smul_mem (degreeLT R (Fintype.card n - 1)) ↑↑(Equiv.Perm.sign c)
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)
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)
rw [mem_degreeLT]
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)
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)
apply lt_of_le_of_lt degree_le_natDegree _
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)
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)
rw [Nat.cast_withBot, Nat.cast_withBot]
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
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)
rw [WithBot.coe_lt_coe]
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)
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
apply lt_of_le_of_lt _ (Equiv.Perm.fixed_point_card_lt_of_ne_one (ne_of_mem_erase hc))
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)
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)
apply le_trans (Polynomial.natDegree_prod_le univ fun i : n => charmatrix M (c i) i) _
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
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)
rw [card_eq_sum_ones]
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
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
rw [sum_filter]
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
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
apply sum_le_sum
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
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
intros
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
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
apply charmatrix_apply_natDegree_le