English
Let (α_i) be a family of types with multiplication. For every index i and elements x, y in α_i, the function that places x·y at position i and zeros elsewhere preserves multiplication: single i (x · y) = (single i x) · (single i y).
Русский
Пусть (α_i) — семейство множеств с операцией умножения. Для любого индекса i и элементов x, y ∈ α_i верно, что функция, возвращающая x·y в позиции i и нулевые значения на остальных позициях, сохраняет умножение: single i (x · y) = single i x · single i y.
LaTeX
$$$\forall i\in\iota, x,y\in\alpha_i:\quad \operatorname{single}_i(x\cdot y) = \operatorname{single}_i(x) \cdot \operatorname{single}_i(y).$$$
Lean4
theorem single_mul (i : ι) (x y : α i) : single i (x * y) = single i x * single i y :=
(MulHom.single _).map_mul _ _
