English
The collection of multilinear maps is an additive commutative group under pointwise addition and negation; the zero map serves as the identity.
Русский
Множество много-линейных отображений образует коммутативную аддитивную группу под покоcкой сложения по точкам и отрицанием; нулевое отображение является единицей.
LaTeX
$$$f + g$ and $-f$ are defined pointwise by $(f+g)(m)=f(m)+g(m)$ and $(-f)(m)=-f(m)$; $0$ is the zero map.$$
Lean4
instance : AddCommGroup (MultilinearMap R M₁ M₂) :=
{
MultilinearMap.addCommMonoid with
neg_add_cancel := fun _ => MultilinearMap.ext fun _ => neg_add_cancel _
sub_eq_add_neg := fun _ _ => MultilinearMap.ext fun _ => sub_eq_add_neg _ _
zsmul := fun n f =>
{ toFun := fun m => n • f m
map_update_add' := fun m i x y => by simp [smul_add]
map_update_smul' := fun l i x d => by simp [← smul_comm x n (_ : M₂)] }
zsmul_zero' := fun _ => MultilinearMap.ext fun _ => SubNegMonoid.zsmul_zero' _
zsmul_succ' := fun _ _ => MultilinearMap.ext fun _ => SubNegMonoid.zsmul_succ' _ _
zsmul_neg' := fun _ _ => MultilinearMap.ext fun _ => SubNegMonoid.zsmul_neg' _ _ }
