instModule — Mathlib

English

If R is a semiring, M an AddCommMonoid, and M is an R-module, then Germ(l, M) is an R-module.

Русский

Если R — полуприводная полукольцо (semiring), M — коммутативное аддитивное моноиде, и существует действие R на M, то Germ(l, M) образует модуль над R.

LaTeX

$$$\\mathrm{Module}(R, \\mathrm{Germ}(l,M))$$$

Lean4

instance instModule [Semiring R] [AddCommMonoid M] [Module R M] : Module R (Germ l M)
    where
  add_smul c₁ c₂
    f :=
    inductionOn f fun f => by
      norm_cast
      simp [add_smul]
  zero_smul
    f :=
    inductionOn f fun f => by
      norm_cast
      simp [zero_smul]

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