sub_mem

Mathlib.RingTheory.TwoSidedIdeal.Basic

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

English

If x,y ∈ I, then x − y ∈ I.

Русский

Если x,y ∈ I, то x − y ∈ I.

LaTeX

$$$x \in I$ и $y \in I$ ⇒ $x-y \in I$$$

Lean4

theorem sub_mem {x y} (hx : x ∈ I) (hy : y ∈ I) : x - y ∈ I :=
  _root_.sub_mem hx hy

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

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

Разделы

Аффилиация

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