instModule' — Mathlib

English

Similarly, Germ(l,R) acts as a ring on Germ(l,M), giving a module structure on Germ(l,M) over Germ(l,R).

Русский

Аналогично Germ(l,R) образует модуль над Germ(l,M).

LaTeX

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

Lean4

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

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