# Addition and subtraction are linear maps from the product space #

Note that these results use `IsLinearMap`, which is mostly discouraged.

## Tags #

linear algebra, vector space, module

source
theorem IsLinearMap.isLinearMap_add {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :
IsLinearMap R fun (x : M × M) => x.1 + x.2
source
theorem IsLinearMap.isLinearMap_sub {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] :
IsLinearMap R fun (x : M × M) => x.1 - x.2