no goals
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i j : n
h : i ≠ j
⊢ charmatrix M i j = -↑C (M i j)
simp only [charmatrix, RingHom.mapMatrix_apply, sub_apply, scalar_apply_ne _ _ _ h, map_apply,
  sub_eq_neg_self]