mulDistribMulAction — Mathlib

English

If α is a Monoid with MulDistribMulAction by R' on α, then the induced action by S ≤ R' is MulDistribMulAction on α.

Русский

Если α — моноид, действует распределённо умножением R' на α, то ограниченное по S действие S на α сохраняет свойствa распределённости.

LaTeX

$$$MulDistribMulAction S \ α$$$

Lean4

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

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