instDistribMulActionOfIsScalarTower

English

There exists a DistribMulAction on AdjoinRoot f compatible with scalar towers, arising from the quotient construction.

Русский

Существует совместимое DistribMulAction на AdjoinRoot f, совместимое с башнями скаляров, полученное через факторную конструкцию.

LaTeX

$$$DistribMulAction S (AdjoinRoot f)$ with IsScalarTower$$

Lean4

instance [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (f : R[X]) : DistribMulAction S (AdjoinRoot f) :=
  Submodule.Quotient.distribMulAction' _

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