Mathlib.Algebra.Module.LinearMap.Prod

Module docstring

{"# 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

IsLinearMap.isLinearMap_add theorem

[AddCommMonoid M] [Module R M] : IsLinearMap R fun x : M × M => x.1 + x.2

Full source

theorem isLinearMap_add [AddCommMonoid M] [Module R M] :
    IsLinearMap R fun x : M × M => x.1 + x.2 := by
  apply IsLinearMap.mk
  · intro x y
    simp only [Prod.fst_add, Prod.snd_add]
    abel
  · intro x y
    simp [smul_add]

Addition is a linear map on product modules

Informal description

Let $M$ be an additive commutative monoid equipped with a module structure over a semiring $R$. Then the addition operation $(x, y) \mapsto x + y$ from $M \times M$ to $M$ is a linear map.

IsLinearMap.isLinearMap_sub theorem

[AddCommGroup M] [Module R M] : IsLinearMap R fun x : M × M => x.1 - x.2

Full source

theorem isLinearMap_sub [AddCommGroup M] [Module R M] :
    IsLinearMap R fun x : M × M => x.1 - x.2 := by
  apply IsLinearMap.mk
  · intro x y
    simp [add_comm, add_assoc, add_left_comm, sub_eq_add_neg]
  · intro x y
    simp [smul_sub]

Subtraction is a linear map on product modules

Informal description

Let $M$ be an additive commutative group equipped with a module structure over a semiring $R$. The subtraction operation $(x, y) \mapsto x - y$ from $M \times M$ to $M$ is a linear map.