posFittingComp_le_iInf_lowerCentralSeries

English

The posFittingComp is contained in the infimum over k of the lower central series of the Lie module.

Русский

Компонента posFitting содержит в себе пересечение по всем k-му понижающей серии нижней центральной для данного модуля Ли.

LaTeX

$$$\operatorname{posFittingComp}(R,L,M) \leq \bigwedge_{k} \operatorname{lowerCentralSeries}(R,L,M,k)$$

Lean4

theorem posFittingComp_le_iInf_lowerCentralSeries : posFittingComp R L M ≤ ⨅ k, lowerCentralSeries R L M k := by
  simp [posFittingComp]

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