smulCommClass — Mathlib

English

For a suitable α acting on R with an IsScalarTower, the induced scalar action on the quotient R/I commutes with the scalar action coming from α on R/I.

Русский

При подходящем α, действующем на R с IsScalarTower, индуцированное скалярное действие на факторе R/I коммутирует с действием α на R/I.

LaTeX

$$SMulCommClass α (R / I) (R / I)$$

Lean4

instance smulCommClass {α} [SMul α R] [IsScalarTower α R R] [SMulCommClass α R R] : SMulCommClass α (R ⧸ I) (R ⧸ I) :=
  (Quotient.ringCon I).smulCommClass

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