map_neg — Mathlib

English

Let f be a Lie module homomorphism between Lie modules M → N over R with a Lie action by L. Then f preserves negation: for every x ∈ M, f(-x) = -f(x).

Русский

Пусть f — гомоморфизм Ли-модуля M → N. Тогда он сохраняет отрицание: для каждого x ∈ M выполняется f(-x) = -f(x).

LaTeX

$$$\forall x \in M,\ f(-x) = -f(x)$$$

Lean4

@[simp]
theorem map_neg (f : M →ₗ⁅R,L⁆ N) (x : M) : f (-x) = -f x :=
  LinearMap.map_neg (f : M →ₗ[R] N) x

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