lie_coe_mem_lie

Mathlib.Algebra.Lie.IdealOperations

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

English

If x ∈ I and m ∈ N, then [x,m] ∈ [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_coe_mem_lie (x : I) (m : N) : ⁅(x : L), (m : M)⁆ ∈ ⁅I, N⁆ := by rw [lieIdeal_oper_eq_span];
  apply subset_lieSpan; use x, m

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

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

Разделы

Аффилиация

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