toAdd_vadd — Mathlib

English

For a ∈ Multiplicative α, the image toAdd of a acts on b by the same α-action, i.e. (a.toAdd) +ᵥ b = a • b.

Русский

Для a ∈ Multiplicative α образ toAdd действует на b тем же самым α-действием: (a.toAdd) +ᵥ b = a • b.

LaTeX

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

Lean4

@[simp]
theorem toAdd_vadd [VAdd α β] (a : Multiplicative α) (b : β) : (a.toAdd : α) +ᵥ b = a • b :=
  rfl

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