Documentation
Mathlib
.
Data
.
Matrix
.
CharP
Search
Google site search
Mathlib
.
Data
.
Matrix
.
CharP
source
Imports
Init
Mathlib.Algebra.CharP.Basic
Mathlib.Data.Matrix.Basic
Imported by
Matrix
.
charP
Matrices in prime characteristic
#
source
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