instTop

Mathlib.Algebra.Lie.Submodule

URI: https://scilib.ai/kg/mathlib#LieSubmodule.instTop

English

For x in M, membership in bottom equals x = 0 (simplified form).

Русский

Для x ∈ M верно: x ∈ ⊥ ⇔ x = 0 (упрощённая форма).

LaTeX

$$$ x \in (⊥ : LieSubmodule R L M) \leftrightarrow x = 0 $$$

Lean4

instance : Top (LieSubmodule R L M) :=
  ⟨{ (⊤ : Submodule R M) with lie_mem := fun {x m} _ ↦ mem_univ ⁅x, m⁆ }⟩

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

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

Разделы

Аффилиация

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