mem_engel_iff — Mathlib

English

Let x and y be elements of a Lie algebra L over a commutative ring R. Then y lies in the Engel subalgebra engel(R, x) if and only if some iterate of the adjoint map ad_R L x kills y, i.e. there exists n ∈ ℕ with (ad_R L x)^n(y) = 0.

Русский

Пусть x, y ∈ L. Тогда y ∈ engel(R, x) тогда и только тогда, когда существует натуральное n такое, что (ad_R L x)^n(y) = 0.

LaTeX

$$$y \in \operatorname{engel}(R,x) \iff \exists n \in \mathbb{N}, ((\operatorname{ad} R L x)^n) y = 0$$$

Lean4

theorem mem_engel_iff (x y : L) : y ∈ engel R x ↔ ∃ n : ℕ, ((ad R L x) ^ n) y = 0 :=
  (Module.End.mem_maxGenEigenspace _ _ _).trans <| by simp only [zero_smul, sub_zero]

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