isLinearMap_add — Mathlib

English

The function sending (x,y) to x + y on a module M is linear over R; in particular, addition on the product M × M is linear.

Русский

Функция, отправляющая пары (x,y) в x + y на модуле M, линейна над R; в частности, сложение на произведении M × M линейно.

LaTeX

$$IsLinearMap R (fun x : M × M => x.1 + x.2)$$

Lean4

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
  · simp [smul_add]

Похожие утверждения