English
Let H be a nontrivial nilpotent Lie subalgebra of L over a commutative ring R. Then the zero-weight space with respect to H, denoted genWeightSpace L 0, contains a nonzero element; i.e., there exists a nonzero vector in the zero-weight space.
Русский
Пусть H — ненулевой нильпотентный подалгебра Ли L над кольцом R. Тогда нулевое весовое пространство genWeightSpace L 0 относительно H непусто, то есть содержит ненулевой вектор.
LaTeX
$$$\exists x \in genWeightSpace\,L\,(0):\ x \neq 0$$$
Lean4
/-- This enables the instance `Zero (Weight R H L)`. -/
instance [Nontrivial H] : Nontrivial (genWeightSpace L (0 : H → R)) :=
by
obtain ⟨⟨x, hx⟩, ⟨y, hy⟩, e⟩ := exists_pair_ne H
exact
⟨⟨x, toLieSubmodule_le_rootSpace_zero R L H hx⟩, ⟨y, toLieSubmodule_le_rootSpace_zero R L H hy⟩, by simpa using e⟩
