lie_bot

Mathlib.Algebra.Lie.IdealOperations

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

English

The bracket with the bottom ideal is bottom: [I, ⊥] = ⊥; similarly [⊥, N] = ⊥.

Русский

Скобка с нижним идеалом равна нулю: [I, ⊥] = ⊥; аналогично [⊥, N] = ⊥.

LaTeX

$$$$ [I, (\bot: LieSubmodule R L M)] = \bot \quad\text{and}\quad [\bot, N] = \bot. $$$$

Lean4

@[simp]
theorem lie_bot : ⁅I, (⊥ : LieSubmodule R L M)⁆ = ⊥ := by rw [eq_bot_iff]; apply lie_le_right

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

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

Разделы

Аффилиация

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