isScalarTower_right — Mathlib

English

If I is a two-sided ideal and α acts on R with a scalar tower over R, then the induced action on the quotient is compatible: IsScalarTower α (R/I) (R/I).

Русский

Если I — двусторонний идеал и альфа действует на R с тензорной (скалярной) башней над R, то индуцированное действие на фактор-кольце совместимо: IsScalarTower α (R/I) (R/I).

LaTeX

$$IsScalarTower α (R \ / I) (R \ / I)$$

Lean4

instance (priority := 100) isScalarTower_right {α} [SMul α R] [IsScalarTower α R R] : IsScalarTower α (R ⧸ I) (R ⧸ I) :=
  (Quotient.ringCon I).isScalarTower_right

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