smul_apply — Mathlib

English

Let (R_i) be a family of modules equipped with a group action on each fiber. The action of G on the restricted product is defined componentwise, so the i-th coordinate of g · x equals g acted on the i-th coordinate: (g · x)_i = g · x_i.

Русский

Пусть имеется семейство модулей (R_i) с действием группы G на каждом элементе. Действие G на ограниченном произведении задано по координатам: (g · x)_i = g · x_i.

LaTeX

$$$ (g \cdot x)_i = g \cdot x_i \quad (\forall i). $$$

Lean4

@[to_additive (attr := simp)]
theorem smul_apply {G : Type*} [Π i, SMul G (R i)] [∀ i, SMulMemClass (S i) G (R i)] (g : G) (x : Πʳ i, [R i, B i]_[𝓕])
    (i : ι) : (g • x) i = g • x i :=
  rfl

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