English
Let f and g be multilinear maps. Their difference f − g is again a multilinear map, defined by (f − g)(m) = f(m) − g(m) for every input m. In particular, subtraction is performed pointwise at each coordinate.
Русский
Пусть f и g — многолинейные отображения. Их разность f − g снова является много-линейным отображением и определяется по правилу (f − g)(m) = f(m) − g(m) для каждого аргумента m. Вычитание выполняется по координатам.
LaTeX
$$$$(f - g)(m) = f(m) - g(m).$$$$
Lean4
instance : Sub (MultilinearMap R M₁ M₂) :=
⟨fun f g =>
⟨fun m => f m - g m, fun m i x y =>
by
simp only [MultilinearMap.map_update_add, sub_eq_add_neg, neg_add]
abel, fun m i c x => by simp only [MultilinearMap.map_update_smul, smul_sub]⟩⟩
