instMulActionSubtypeMem — Mathlib

English

The action by a subring is the same as the action by the ambient ring, i.e., restricting the ring action to S makes S act on α the same way as R does.

Русский

Действие подкольца на модуле совпадает с действием всего кольца, то есть ограничение действия на S совпадает с исходным действием R.

LaTeX

$$$MulAction\; S\; \alpha$$$

Lean4

/-- The action by a subring is the action by the underlying ring. -/
instance [MulAction R α] (S : Subring R) : MulAction S α :=
  inferInstanceAs (MulAction S.toSubsemiring α)

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