instDistribMulActionSubtypeMem — Mathlib

English

There is a DistribMulAction of S on α, inherited from the ambient action, satisfying distributivity of scalars over addition.

Русский

Существует DistribMulAction S на α, унаследованный от внешнего действия, удовлетворяющий распределение по сложению над скалярами.

LaTeX

$$$\text{DistribMulAction } S \alpha$$$

Lean4

/-- The action by a subalgebra is the action by the underlying algebra. -/
instance [AddMonoid α] [DistribMulAction A α] (S : Subalgebra R A) : DistribMulAction S α :=
  inferInstanceAs (DistribMulAction S.toSubsemiring α)

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