isLinearMap_sub — Mathlib

English

The function sending (x,y) to x − y on a module M is linear over R; subtraction is linear in each argument.

Русский

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

LaTeX

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

Lean4

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

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