Matrices in prime characteristic

In this file we prove that matrices over a ring of characteristic p with nonempty index type have the same characteristic.

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

instance Matrix.instCharZero {n : Type u_1} {R : Type u_2} [DecidableEq n] [Nonempty n] [AddMonoidWithOne R] [CharZero R] : CharZero (Matrix n n R)

instance Matrix.instExpChar {n : Type u_1} {R : Type u_2} [DecidableEq n] [Nonempty n] [AddMonoidWithOne R] {p : ℕ} [ExpChar R p] : ExpChar (Matrix n n R) p