instSMulOfIsScalarTower — Mathlib

English

Base change preserves the lower central series: the k-th lowerCentralSeries of A acting on A⊗R L with A⊗R M equals the base-changed k-th lowerCentralSeries of R acting on L on M.

Русский

Базовое изменение сохраняет нижнюю центральную серию: k-я lowerCentralSeries(A, A⊗R L, A⊗R M) совпадает с базовым изменением k-й lowerCentralSeries(R,L,M).

LaTeX

$$$\operatorname{lowerCentralSeries} A (A \otimes_R L) (A \otimes_R M) k = (\operatorname{lowerCentralSeries} R L M k).baseChange A$$$

Lean4

instance {S : Type*} [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] : SMul S (FreeLieAlgebra R X) where
  smul t := Quot.map (t • ·) (Rel.smulOfTower t)

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