instMulDistribMulActionSubtypeMem

English

Restriction of a MulDistribMulAction from R to a subring S gives a MulDistribMulAction of S on α.

Русский

Ограничение MulDistribMulAction от R до подкольца S задаёт MulDistribMulAction на α для S.

LaTeX

$$$MulDistribMulAction\; S\; \alpha$$$

Lean4

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

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