instIsTwoSided

Mathlib.RingTheory.Ideal.Defs

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

English

In a commutative semiring, every ideal is two-sided.

Русский

В коммутативном полупрямом кольце каждый идеал двусторонний.

LaTeX

$$$\forall \alpha\; [\text{CommSemiring } \alpha], \; \forall I \; (I: \text{Ideal } \alpha) : I \text{IsTwoSided}. $$$

Lean4

instance : I.IsTwoSided :=
  ⟨fun b ha ↦ mul_comm b _ ▸ I.smul_mem _ ha⟩

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

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

Разделы

Аффилиация

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