instDistribSMul — Mathlib

English

If R is a ring and V a module with scalar action, the smul distributes over addition in the base ring: (r + s) • u = r • u + s • u for all r, s ∈ R and u ∈ V. This extends to the Hahn module action as well.

Русский

Если R — кольцо и V модуль с действиями скаляров, распределение выполняется над сложением в базовом кольце: (r + s) • u = r • u + s • u для всех r, s ∈ R и u ∈ V. Это распространяется и на действие Hahn-модуля.

LaTeX

$$$ (r + s) \cdot u = r \cdot u + s \cdot u \, (\text{for all } r,s,u) $$$

Lean4

instance instDistribSMul [MonoidWithZero R] [DistribSMul R V] : DistribSMul (HahnSeries Γ R) (HahnModule Γ' R V) where
  smul_add := smul_add

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