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.charP {n : Type u_1} {R : Type u_2} [AddMonoidWithOne R] [DecidableEq n] [Nonempty n] (p : ℕ) [CharP R p] : CharP (Matrix n n R) p

Equations

• (_ : CharP (Matrix n n R) p) = (_ : CharP (Matrix n n R) p)