English
Under nondegeneracy and invariance assumptions for a bilinear form Φ on a Lie algebra L, the lattice of Lie ideals is generated by atoms: for every I, the supremum of atoms J with J ≤ I equals I.
Русский
При ненегативности и инвариантности билинейной формы Φ на Ли-алгебре L множество идeалов образуется из атомов: для каждого I наивысшая сверху над атомами J, удовлетворяющими J ⊆ I, равна I.
LaTeX
$$$$ \forall I,\; \sup\{ J : \text{IsAtom}(J) \land J \le I \} = I. $$$$
Lean4
/-- A bilinear form on a Lie module `M` of a Lie algebra `L` is *invariant* if
for all `x : L` and `y z : M` the condition `Φ ⁅x, y⁆ z = -Φ y ⁅x, z⁆` holds.
-/
def _root_.LinearMap.BilinForm.lieInvariant : Prop :=
∀ (x : L) (y z : M), Φ ⁅x, y⁆ z = -Φ y ⁅x, z⁆
