instMulAction' — Mathlib

English

There is a MulAction of Germ(l, M) on Germ(l, β).

Русский

Существует действие MulAction \\mathrm{Germ}(l, M) на \\mathrm{Germ}(l, β).

LaTeX

$$$\\mathrm{MulAction}(\\mathrm{Germ}(l,M), \\mathrm{Germ}(l,\\beta))$$$

Lean4

@[to_additive]
instance instMulAction' [Monoid M] [MulAction M β] : MulAction (Germ l M) (Germ l β)
    where
  one_smul f := inductionOn f fun f => by simp only [← coe_one, ← coe_smul', one_smul]
  mul_smul c₁ c₂
    f :=
    inductionOn₃ c₁ c₂ f fun c₁ c₂ f => by
      norm_cast
      simp [mul_smul]

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