Matrices in prime characteristic

instance Matrix.charP {n : Type u_1} [Fintype n] {R : Type u_2} [Ring R] [DecidableEq n] [Nonempty n] (p : ℕ) [CharP R p] : CharP (Matrix n n R) p