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]
:
Equations
- ⋯ = ⋯