Documentation
Mathlib
.
RingTheory
.
SimpleRing
.
Matrix
Search
Google site search
return to top
source
Imports
Init
Mathlib.LinearAlgebra.Matrix.Ideal
Mathlib.RingTheory.SimpleRing.Basic
Imported by
IsSimpleRing
.
matrix
The matrix ring over a simple ring is simple
source
instance
IsSimpleRing
.
matrix
(ι :
Type
u_1)
(A :
Type
u_2)
[
Ring
A
]
[
Fintype
ι
]
[
Nonempty
ι
]
[
IsSimpleRing
A
]
:
IsSimpleRing
(
Matrix
ι
ι
A
)