of_isSimpleRing

Mathlib.RingTheory.SimpleRing.Principal

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

English

If R is a commutative simple ring, then R is a domain (an integral domain).

Русский

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

LaTeX

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

Lean4

instance of_isSimpleRing : IsDomain R :=
  ((isSimpleRing_iff_isField _).mp ‹_›).isDomain

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

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

Разделы

Аффилиация

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