instNontrivial — Mathlib

English

There exists a finite index n and a matrix algebra over the opposite End of a simple module, isomorphic to the ring.

Русский

Существуют конечный индекс n и матричные алгебры над противоположной End-модулями, изоморфные кольцу.

LaTeX

$$$\\exists n, I, (\\mathrm{End}_R(I))^{op}, R \\cong \\mathrm{Mat}_n(I)^{op}$$$

Lean4

instance [IsSimpleRing R] : Nontrivial R :=
  by
  obtain ⟨x, _, hx⟩ := SetLike.exists_of_lt (bot_lt_top : (⊥ : TwoSidedIdeal R) < ⊤)
  use x, 0, hx

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