instSMulZeroClass — Mathlib

English

Let x be a Hahn series and 0 the zero element of the Hahn module. The action of x on the zero vector is the zero vector: x · 0 = 0.

Русский

Пусть x — Ханнова серия, а 0 — нулевой элемент Hahn-модуля. Действие x на нулевой вектор даёт нулевой вектор: x · 0 = 0.

LaTeX

$$$ x \cdot 0 = 0 $$$

Lean4

instance instSMulZeroClass [SMulZeroClass R V] : SMulZeroClass (HahnSeries Γ R) (HahnModule Γ' R V) where
  smul_zero
    x := by
    ext
    simp [coeff_smul]

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