toMul_smul — Mathlib

English

For every a in Additive α and b in β, the action of a, viewed through the toMul tag, coincides with the original α-action on β.

Русский

Для каждого a в Additive α и b в β действие a, рассмотренное через тег toMul, совпадает с исходным действием α на β.

LaTeX

$$$ (a^{\\mathrm{toMul}} : \\alpha) \\;\\cdot\\; b = a +\\!\\!\\!\\! \\_ b$$$

Lean4

@[simp]
theorem toMul_smul [SMul α β] (a : Additive α) (b : β) : (a.toMul : α) • b = a +ᵥ b :=
  rfl

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