instDistribMulAction — Mathlib

English

If M acts on N and N is a ring, then M acts on Germ(l, N) distributively.

Русский

Если M действует на N и N является кольцом, то M действует на Germ(l,N) дистрибутивно.

LaTeX

$$$[Monoid M] [AddMonoid N] [DistribMulAction M N] \Rightarrow DistribMulAction M (Germ(l,N))$$$

Lean4

instance instDistribMulAction [Monoid M] [AddMonoid N] [DistribMulAction M N] : DistribMulAction M (Germ l N)
    where
  smul_add c f
    g :=
    inductionOn₂ f g fun f g => by
      norm_cast
      simp [smul_add]
  smul_zero c := by simp only [← coe_zero, ← coe_smul, smul_zero]

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