mulAction — Mathlib

English

If α has a MulAction by R' and S ⊆ R' is a subsemiring, then α inherits a MulAction by S by restriction of scalars; the action of S on α is the same as the action of R' restricted to S.

Русский

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

LaTeX

$$$MulAction S \ α$$$

Lean4

/-- The action by a subsemiring is the action by the underlying semiring. -/
instance mulAction [MulAction R' α] (S : Subsemiring R') : MulAction S α :=
  inferInstance

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