zero_mem

Mathlib.RingTheory.TwoSidedIdeal.Basic

URI: https://scilib.ai/kg/mathlib#TwoSidedIdeal.zero_mem

English

Let I be a two-sided ideal in a nonunital, nonassociative ring R. Then the zero element belongs to I.

Русский

Пусть I — двусторонний идеал в кольце без единицы и без ассоциативности R. Тогда ноль принадлежит I.

LaTeX

$$$0 \in I$$$

Lean4

theorem zero_mem : 0 ∈ I :=
  I.ringCon.refl 0

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

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

Разделы

Аффилиация

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