lie_eq_self_of_isAtom_of_ne_bot — Mathlib

English

Let I be a Lie ideal and N an atom submodule of a Lie module. If [I,N] ≠ ⊥ (i.e., the bracket of I with N is nontrivial), then the bracket [I,N] equals N; equivalently, N is generated by its bracket with I.

Русский

Пусть I — идеал Ли, N — атомарное подмодуль. Если [I,N] не нуль, то [I,N] = N; то есть N порождается скобкой с I.

LaTeX

$$$[I,N] = N$ при IsAtom(N) и [I,N] \neq \{0\}$$$

Lean4

theorem lie_eq_self_of_isAtom_of_ne_bot (hN : IsAtom N) (h : ⁅I, N⁆ ≠ ⊥) : ⁅I, N⁆ = N :=
  (hN.le_iff_eq h).mp <| LieSubmodule.lie_le_right N I

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