no goals
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
split_ifs with h <;> simp [h, natDegree_X_sub_C_le]