instIsTwoSided_1

Mathlib.RingTheory.Ideal.Defs

URI: https://scilib.ai/kg/mathlib#Ideal.instIsTwoSided_1

English

In a commutative ring, any ideal is two-sided.

Русский

В коммутативном кольце любой идеал двусторонний.

LaTeX

$$$\forall I\; (I: \text{Ideal } \alpha)\; I^{{\text{IsTwoSided}}}$.$$

Lean4

instance {α} [CommRing α] (I : Ideal α) : I.IsTwoSided :=
  inferInstance

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

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

Разделы

Аффилиация

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