trivial_lie_oper_zero — Mathlib

English

Let I be an atom LieIdeal. If ⁅I,I⁆ ≠ ⊥, then ⁅I,I⁆ = I.

Русский

Пусть I — атомный Ли-идеал. Если ⁅I,I⁆ не равно нулю, то ⁅I,I⁆ = I.

LaTeX

$$$IsAtom(I) \rightarrow (⁅I,I⁆ \neq \bot) \Rightarrow ⁅I,I⁆ = I$$$

Lean4

@[simp]
theorem trivial_lie_oper_zero [LieModule.IsTrivial L M] : ⁅I, N⁆ = ⊥ :=
  by
  suffices ⁅I, N⁆ ≤ ⊥ from le_bot_iff.mp this
  rw [lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le]
  rintro m ⟨x, n, h⟩; rw [trivial_lie_zero] at h; simp [← h]

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