instDistribMulActionSubtypeMem — Mathlib

English

If α has a distributive action of R on α, then S-subring yields a DistribMulAction of S on α by restriction.

Русский

Если у α есть распределительное действие R на α, то подкольцо S задаёт DistribMulAction на α посредством ограничения.

LaTeX

$$$DistribMulAction\; S\; \alpha$$$

Lean4

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

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