instNeg — Mathlib

English

The negation of a linear map is linear: if f: M →ₛₗ[σ₁₂] N₂, then -f is linear.

Русский

Отрицание линейного отображения линейно: если f: M →ₛₗ[σ₁₂] N₂, то -f линейно.

LaTeX

$$Neg (M →ₛₗ[σ₁₂] N₂)$$

Lean4

/-- The negation of a linear map is linear. -/
instance : Neg (M →ₛₗ[σ₁₂] N₂) :=
  ⟨fun f ↦
    { toFun := -f
      map_add' := by simp [add_comm]
      map_smul' := by simp }⟩

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