instMulAction — Mathlib

English

Instance giving a MulAction on the carrier of X in Action.FintypeCat, via the previous instance.

Русский

Инстанс MulAction на носитель X в Action.FintypeCat через предыдущий инстанс.

LaTeX

$$$\text{instMulActionCarrier}$$$

Lean4

instance instMulAction {G : Type*} [Monoid G] (X : Action V G) : MulAction G (ToType X)
    where
  smul g x := ConcreteCategory.hom (X.ρ g) x
  one_smul
    x := by
    change ConcreteCategory.hom (X.ρ 1) x = x
    simp
  mul_smul g h
    x :=
    by
    change ConcreteCategory.hom (X.ρ (g * h)) x = ConcreteCategory.hom (X.ρ g) ((ConcreteCategory.hom (X.ρ h)) x)
    simp
      /- Specialize `instMulAction` to assist typeclass inference. -/

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