isScalarTower_right — Mathlib

English

If S acts on R via a monoid action, AdjoinRoot f inherits a DistribMulAction from the quotient structure.

Русский

Если S действует на R через моноидальное действие, AdjoinRoot f наследует DistribMulAction через факторную структуру.

LaTeX

$$$DistribMulAction S (AdjoinRoot f)$$$

Lean4

instance isScalarTower_right [DistribSMul S R] [IsScalarTower S R R] : IsScalarTower S (AdjoinRoot f) (AdjoinRoot f) :=
  Ideal.Quotient.isScalarTower_right

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