val_smul — Mathlib

English

The scalar action by G on M lifts to Units M by taking the underlying value; the equality is given by the valuation map.

Русский

Действие скаляра G на M поднимается к Units M через отображение значения; равенство задаётся через изображение значения.

LaTeX

$$$ \\uparrow(g \\cdot m) = g \\cdot (m) $$$

Lean4

@[to_additive (attr := simp)]
theorem val_smul [Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M] [IsScalarTower G M M] (g : G) (m : Mˣ) :
    ↑(g • m) = g • (m : M) :=
  rfl

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