mathlib documentation

data.matrix.char_p

Matrices in prime characteristic #

source
@[protected, instance]
def matrix.char_p {n : Type u_1} [fintype n] {R : Type u_2} [ring R] [decidable_eq n] [nonempty n] (p : ℕ) [char_p R p] :
char_p (matrix n n R) p