map_neg — Mathlib

English

Negating the input commutes with Ray.map: map f (-v) = -map f v for any linear equivalence f.

Русский

Отрицание входа коммутирует с Ray.map: map f (-v) = -map f v для любого линейного равномножителя f.

LaTeX

$$$map\ f\ (-v) = -map\ f\ v$.$$

Lean4

@[simp]
protected theorem map_neg (f : M ≃ₗ[R] N) (v : Module.Ray R M) : map f (-v) = -map f v := by
  induction v using Module.Ray.ind with
  | h g hg => simp

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