smul — Mathlib

English

There is an action of S on p defined by applying the action to representatives and packaging back into p.

Русский

Определено действие S на p через применение к представителям и возврат в p.

LaTeX

$$$ \\text{definition of } p \\text{ as an } S\\text{-module with } c\\cdot x := \\langle c\\cdot x, \\text{proof } \\rangle$$$

Lean4

instance smul [SMul S R] [SMul S M] [IsScalarTower S R M] : SMul S p :=
  ⟨fun c x => ⟨c • x.1, smul_of_tower_mem _ c x.2⟩⟩

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