lie_abelian_iff_lie_self_eq_bot — Mathlib

English

For an atom I, if I is not LieAbelian, then ⁅I,I⁆ = I.

Русский

Для атома I, если I не абелево, то ⁅I,I⁆ = I.

LaTeX

$$IsAtom I → Not IsLieAbelian I → ⁅I,I⁆ = I$$

Lean4

theorem lie_abelian_iff_lie_self_eq_bot : IsLieAbelian I ↔ ⁅I, I⁆ = ⊥ :=
  by
  simp only [_root_.eq_bot_iff, lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le, LieSubmodule.bot_coe,
    Set.subset_singleton_iff, Set.mem_setOf_eq, exists_imp]
  refine
    ⟨fun h z x y hz =>
      hz.symm.trans
        (((I : LieSubalgebra R L).coe_bracket x y).symm.trans ((coe_zero_iff_zero _ _).mpr (by apply h.trivial))),
      fun h => ⟨fun x y => ((I : LieSubalgebra R L).coe_zero_iff_zero _).mp (h _ x y rfl)⟩⟩

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