instMulOpposite

Mathlib.RingTheory.SimpleRing.Basic

URI: https://scilib.ai/kg/mathlib#IsSimpleRing.instMulOpposite

English

If a ring R is simple, then its opposite ring R^op is also simple.

Русский

Если кольцо R простое, то и противоположное кольцо R^op простое.

LaTeX

$$If IsSimpleRing R, then IsSimpleRing R^op.$$

Lean4

instance [IsSimpleRing R] : IsSimpleRing Rᵐᵒᵖ :=
  ⟨TwoSidedIdeal.opOrderIso.symm.isSimpleOrder⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru