mem_bot

Mathlib.RingTheory.Ideal.Lattice

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

English

For any x in the bottom ideal ⊥ of R, x = 0.

Русский

Для любого элемента x в нижнем идеале ⊥ кольца R выполняется x = 0.

LaTeX

$$$x \\in (\\\\perp : \\\\mathrm{Ideal} \\\\ R) \\iff x = 0$$$

Lean4

theorem mem_bot {x : R} : x ∈ (⊥ : Ideal R) ↔ x = 0 :=
  Submodule.mem_bot _

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

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

Разделы

Аффилиация

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