smul — Mathlib

English

The scalar action on the sheafified module equals the application of the SMulCandidate to the scalar and the element.

Русский

Скалярное действие на шейфицированном модуле задаётся через SMulCandidate.

LaTeX

$$$ smul α φ r m = s $ where $ s := (SMulCandidate α φ r m).x $$$

Lean4

/-- The scalar multiplication on the sheafification of a presheaf of modules. -/
noncomputable def smul : A.val.obj X :=
  (smulCandidate α φ r m).x

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