toSubmodule_bot

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalAlgebra.toSubmodule_bot

← MathLib Explorer

English

An element lies in the bottom subalgebra iff it is zero.

Русский

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

LaTeX

$$$ x \\in \\bot \\;\\Leftrightarrow\\; x = 0 $$$

Lean4

theorem toSubmodule_bot : (⊥ : NonUnitalSubalgebra R A).toSubmodule = ⊥ :=
  by
  ext
  simp only [mem_bot, NonUnitalSubalgebra.mem_toSubmodule, Submodule.mem_bot]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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