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
inst✝ : Nontrivial R
i j : n
⊢ natDegree (charmatrix M i j) = if i = j then 1 else 0
by_cases i = j <;> simp [h, ← degree_eq_iff_natDegree_eq_of_pos (Nat.succ_pos 0)]