toAdd_mul — Mathlib

English

The map toAdd preserves multiplication when viewed from Multiplicative α to α: (x * y).toAdd = x.toAdd + y.toAdd.

Русский

Преобразование toAdd сохраняет умножение, когда рассматривается как отображение из Multiplicative α в α: (x*y).toAdd = x.toAdd + y.toAdd.

LaTeX

$$toAdd_mul [Add α] (x y : Multiplicative α) : (x * y).toAdd = x.toAdd + y.toAdd$$

Lean4

@[simp]
theorem toAdd_mul [Add α] (x y : Multiplicative α) : (x * y).toAdd = x.toAdd + y.toAdd :=
  rfl

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