toMulAction — Mathlib

English

The natural MulActionHom induced by subtype acts as the identity on Subtype values.

Русский

Естественный MulActionHom, индуцируемый подтипом, действует как тождественный на значения подтипа.

LaTeX

$$$\\text{SubMulAction.SMulMemClass.subtype} : S' \\to[M] M$$$

Lean4

/-- A `SubMulAction` of a `MulAction` is a `MulAction`. -/
@[to_additive /-- A `SubAddAction` of an `AddAction` is an `AddAction`. -/
    ]
instance (priority := 75) toMulAction : MulAction R S' :=
  Subtype.coe_injective.mulAction Subtype.val (SetLike.val_smul S')

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