English
Let R be a ring, and S ≤ R a subring. If β carries a left R-action and α acts on β with the property that the actions of R and α on β commute, then the restricted action of S on β also commutes with the α-action. In short, the commutativity of actions descends to subrings.
Русский
Пусть R — кольцо, S ⊆ R подкольцо. Пусть β имеет действие слева R на β и α действует на β так, что действия R и α на β коммутируют; тогда ограниченное до S действие S на β также будет коммутировать с действием α. Короче: коммутативность действий спадёт на подкольцо.
LaTeX
$$$SMulCommClass\; S\; \alpha\; \beta$$$
Lean4
instance smulCommClass_left [SMul R β] [SMul α β] [SMulCommClass R α β] (S : Subring R) : SMulCommClass S α β :=
inferInstanceAs (SMulCommClass S.toSubsemiring α β)
