instMulAction — Mathlib

English

There is a natural action of any monoid α on the graded monoid GradedMonoid A; for g ∈ α, i ∈ ι, a ∈ A_i, g · (i,a) = (i, g · a).

Русский

Существует естественное действие любого моноида α на градуированном моноиде GradedMonoid A; для g ∈ α, i ∈ ι, a ∈ A_i выполняется g · (i,a) = (i, g · a).

LaTeX

$$$\forall g \in \alpha, \forall i, \forall a \in A_i:\ g \cdot (i,a) = (i, g \cdot a)$$$

Lean4

instance [Monoid α] [∀ i, MulAction α (A i)] : MulAction α (GradedMonoid A)
    where
  one_smul g := Sigma.ext rfl <| heq_of_eq <| one_smul _ g.2
  mul_smul r₁ r₂ g := Sigma.ext rfl <| heq_of_eq <| mul_smul r₁ r₂ g.2

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