posFittingCompOf_eq_bot_of_isNilpotent

English

If L is nilpotent as a Lie algebra acting on M, then for every x in L the positive Fitting component of x on M is the zero submodule; i.e. posFittingCompOfR M x = ⊥ for all x ∈ L.

Русский

Если L является нильпотентной по отношению к действию на M, то для каждого x ∈ L положительная компонента Фиттинга действия x на M равна нулевому подпомодулю; то есть posFittingCompOf_R M x = ⊥ для всех x в L.

LaTeX

$$$\forall x \in L,\; \operatorname{posFittingCompOf}(R,M,x)=\bot$$$

Lean4

@[simp]
theorem posFittingCompOf_eq_bot_of_isNilpotent [IsNilpotent L M] (x : L) : posFittingCompOf R M x = ⊥ := by
  simp_rw [eq_bot_iff, ← iInf_lowerCentralSeries_eq_bot_of_isNilpotent, le_iInf_iff,
    posFittingCompOf_le_lowerCentralSeries, forall_const]

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