of_isSimpleRing

Mathlib.RingTheory.SimpleRing.Principal

URI: https://scilib.ai/kg/mathlib#IsPrincipalIdealRing.of_isSimpleRing

English

If R is a commutative simple ring, then R is a principal ideal ring.

Русский

Если R — коммутативное простое кольцо, то R является кольцом с принципиальными идеалами.

LaTeX

$$IsPrincipalIdealRing R for [CommRing R] and [IsSimpleRing R].$$

Lean4

instance of_isSimpleRing : IsPrincipalIdealRing R :=
  ((isSimpleRing_iff_isField _).mp ‹_›).isPrincipalIdealRing

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

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

Разделы

Аффилиация

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