matrix — Mathlib

English

If A is a simple ring and ι is a finite nonempty index type, then the matrix ring Matrix ι ι A is simple.

Русский

Если A простое кольцо и ι — конечный ненулевой индекс, то матричное кольцо Matrix ι ι A простое.

LaTeX

$$IsSimpleRing A ⇒ IsSimpleRing (Matrix ι ι A) for finite ι with Nonempty ι.$$

Lean4

instance matrix [IsSimpleRing A] : IsSimpleRing (Matrix ι ι A) where
  simple :=
    letI := Classical.decEq ι;
    TwoSidedIdeal.orderIsoMatrix |>.symm.isSimpleOrder

Похожие утверждения