English
Let α be an additive structure. For any two functions f, g: m → n → α, the embedding of these functions into matrices is additive: the matrix corresponding to f plus the matrix corresponding to g equals the matrix corresponding to f+g.
Русский
Пусть α является добавляемой структурой. Для любых функций f, g: m → n → α вложение функций в матрицы сохраняет сложение: матрица, соответствующая f, плюс матрица, соответствующая g, равна матрице, соответствующей f+g.
LaTeX
$$$ \\forall f,g: m \\to n \\to \\alpha,\\quad \\mathrm{of}(f) + \\mathrm{of}(g) = \\mathrm{of}(f + g) $$$
Lean4
@[simp]
theorem of_add_of [Add α] (f g : m → n → α) : of f + of g = of (f + g) :=
rfl
