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

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

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