smulCommClass_right — Mathlib

English

Let R be a ring, S ≤ R a subring. If α acts on β and there is a commuting relation between α and R on β, restricting R to S yields that α and S act on β commute as well.

Русский

Пусть R — кольцо, S ⊆ R подкольцо. Пусть α действует на β и существует коммутативность действий α и R на β; ограничение до S сохраняет это свойство: α и S действуют на β взаимно приводимо.

LaTeX

$$$SMulCommClass\; \alpha\; S\; \beta$$$

Lean4

instance smulCommClass_right [SMul α β] [SMul R β] [SMulCommClass α R β] (S : Subring R) : SMulCommClass α S β :=
  inferInstanceAs (SMulCommClass α S.toSubsemiring β)

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