Documentation

Mathlib.Data.Matrix.CharP

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