Documentation

Mathlib.Data.Matrix.CharP

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.

theorem 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