ideal_oper_maxTrivSubmodule_eq_bot

English

For any LieIdeal I of L, the bracket of I with the maximal trivial submodule is still trivial, i.e., ⁅I, maxTrivSubmodule R L M⁆ = ⊥.

Русский

Для любого Ли-идеала I подмодуля L скобкой со максимальным тривиальным подмодулем остаётся тривиальность, т.е. ⁅I, maxTrivSubmodule R L M⁆ = ⊥.

LaTeX

$$$⁅I, maxTrivSubmodule R L M⁆ = ⊥$, for every LieIdeal I of L.$$

Lean4

@[simp]
theorem ideal_oper_maxTrivSubmodule_eq_bot (I : LieIdeal R L) : ⁅I, maxTrivSubmodule R L M⁆ = ⊥ :=
  by
  rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.lieIdeal_oper_eq_linear_span, LieSubmodule.bot_toSubmodule,
    Submodule.span_eq_bot]
  rintro m ⟨⟨x, hx⟩, ⟨⟨m, hm⟩, rfl⟩⟩
  exact hm x

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