instModule — Mathlib

English

If V is an R-module and the action is compatible, then HahnSeries Γ V carries an R-module structure extending the one on V; i.e., HahnSeries Γ V is an R-module.

Русский

Если V — модуль над R и действует согласованно, то HahnSeries Γ V наследует структуру R-модуля, расширяющую модульную структуру V.

LaTeX

$$$\\ HahnSeries Γ V \\text{ is an } R\\text{-module}$$$

Lean4

instance : Module R (HahnSeries Γ V) :=
  {
    inferInstanceAs
      (DistribMulAction R
        (HahnSeries Γ
          V)) with
    zero_smul := fun _ => by
      ext
      simp
    add_smul := fun _ _ _ => by
      ext
      simp [add_smul] }

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