mem_bot

Mathlib.Topology.Algebra.Module.ClosedSubmodule

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

English

An element lies in the bottom closed submodule exactly when it is zero.

Русский

Элемент принадлежит нижнему замкнутому подмодулю тогда и только тогда, когда он равен нулю.

LaTeX

$$$x \in (\bot : ClosedSubmodule R M) \iff x = 0$$$

Lean4

@[simp]
theorem mem_bot : x ∈ (⊥ : ClosedSubmodule R M) ↔ x = 0 :=
  .rfl

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

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

Разделы

Аффилиация

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