lie_mem_lie

Mathlib.Algebra.Lie.IdealOperations

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

English

For x ∈ I and m ∈ N, the bracket [x,m] lies in [I,N].

Русский

Для x ∈ I и m ∈ N скобка [x,m] принадлежит [I,N].

LaTeX

$$$$ x \in I \land m \in N \Rightarrow [x,m] \in [I,N]. $$$$

Lean4

theorem lie_mem_lie {x : L} {m : M} (hx : x ∈ I) (hm : m ∈ N) : ⁅x, m⁆ ∈ ⁅I, N⁆ :=
  lie_coe_mem_lie ⟨x, hx⟩ ⟨m, hm⟩

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

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

Разделы

Аффилиация

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