coe_neg — Mathlib

English

The negation of a continuous linear map, viewed as a linear map, coincides with the negation of the original map.

Русский

Отрицание непрерывного линейного отображения, как линейного отображения, совпадает с отрицанием исходного отображения.

LaTeX

$$↑(-f) = -f$$

Lean4

@[simp, norm_cast]
theorem coe_neg (f : M →SL[σ₁₂] M₂) : (↑(-f) : M →ₛₗ[σ₁₂] M₂) = -f :=
  rfl

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