sub_mem

Mathlib.RingTheory.Ideal.Defs

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

English

If a ∈ I and b ∈ I, then a − b ∈ I.

Русский

Если a и b принадлежат I, то их разность a − b принадлежит I.

LaTeX

$$$\forall I\; (I: \text{Ideal } \alpha)\; \forall a,b:\alpha, \; a \in I \rightarrow b \in I \rightarrow a-b \in I.$$$

Lean4

protected theorem sub_mem : a ∈ I → b ∈ I → a - b ∈ I :=
  Submodule.sub_mem I

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

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

Разделы

Аффилиация

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