instModule — Mathlib

English

There is a module structure linking HahnSeries and HahnModule via scalar action.

Русский

Существует структура модуля, связывающая HahnSeries и HahnModule через скалярное действие.

LaTeX

$$$\text{Module}((\mathrm{HahnSeries}\; \Gamma\; R),\ (\mathrm{HahnModule}\; \Gamma'\; R\; V))$$$

Lean4

instance instModule [Semiring R] [Module R V] : Module (HahnSeries Γ R) (HahnModule Γ' R V) :=
  {
    inferInstanceAs (DistribSMul (HahnSeries Γ R)
        (HahnModule Γ' R V)) with
    mul_smul := mul_smul'
    one_smul := fun _ => one_smul'
    add_smul := fun _ _ _ => add_smul Module.add_smul
    zero_smul := fun _ => zero_smul' }

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