instMulActionSubtypeMem — Mathlib

English

If M' acts on α as a MulAction and S' is a Submonoid of M', then α carries a MulAction of S' obtained by restriction of scalars.

Русский

Если M' действует на α как умножение, и S' является подмонойдом M', то на α естественно наследуется действие S' через ограничение по скаларам.

LaTeX

$$$\text{MulAction } S' \alpha\quad\text{with } (s \in S') \text{ acts as } (s\cdot x) \text{ using the same action as in } M'.$$$

Lean4

@[to_additive]
instance (priority := low) [MulAction M' α] : MulAction s α
    where
  one_smul := one_smul M'
  mul_smul m₁ m₂ := mul_smul (m₁ : M') m₂

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