neg_mem_iff

Mathlib.RingTheory.Ideal.Defs

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

English

In a ring, an ideal contains a and its negation −a simultaneously: −a ∈ I ↔ a ∈ I.

Русский

В кольце идеал содержит элемент a и его отрицание −a тогда и только тогда, когда a ∈ I.

LaTeX

$$$\forall a:\alpha,\; (-a) \in I \iff a \in I.$$$

Lean4

protected theorem neg_mem_iff : -a ∈ I ↔ a ∈ I :=
  Submodule.neg_mem_iff I

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

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

Разделы

Аффилиация

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