English
For the diagonal entries i,i of M, the degree of charmatrix entry satisfies an inequality with respect to the index position.
Русский
Для диагональных элементов M_{ii} выполняется неравенство степени соответствующего charmatrix-элемента относительно позиции i.
LaTeX
$$$$ \\operatorname{natDegree}(\\operatorname{charmatrix}(M)_{ii}) \\le 1, $$ для i = i, а для i \\neq i — не более 0.$$
Lean4
theorem charpoly_sub_diagonal_degree_lt : (M.charpoly - ∏ i : n, (X - C (M i i))).degree < ↑(Fintype.card n - 1) :=
by
rw [charpoly, det_apply', ← insert_erase (mem_univ (Equiv.refl n)), sum_insert (notMem_erase (Equiv.refl n) univ),
add_comm]
simp only [charmatrix_apply_eq, one_mul, Equiv.Perm.sign_refl, id, Int.cast_one, Units.val_one, add_sub_cancel_right,
Equiv.coe_refl]
rw [← mem_degreeLT]
apply Submodule.sum_mem (degreeLT R (Fintype.card n - 1))
intro c hc; rw [← C_eq_intCast, C_mul']
apply Submodule.smul_mem (degreeLT R (Fintype.card n - 1)) ↑↑(Equiv.Perm.sign c)
rw [mem_degreeLT]
apply lt_of_le_of_lt degree_le_natDegree _
rw [Nat.cast_lt]
apply lt_of_le_of_lt _ (Equiv.Perm.fixed_point_card_lt_of_ne_one (ne_of_mem_erase hc))
apply le_trans (Polynomial.natDegree_prod_le univ fun i : n => charmatrix M (c i) i) _
rw [card_eq_sum_ones]; rw [sum_filter]; apply sum_le_sum
intros
apply charmatrix_apply_natDegree_le
