negation on module as linear map

Stream: Is there code for X?

[Kevin Buzzard]

I can't find this:

import Mathlib.Algebra.Module.LinearMap.Basic

def LinearMap.neg (R : Type*) [Ring R] (A : Type*) [AddCommGroup A] [Module R A] : A →ₗ[R] A where
  toFun := (-·)
  map_add' := neg_add
  map_smul' r a := (smul_neg r a).symm

Do we not have it? Do we not want it for some reason? Have I named it correctly?

[Ruben Van de Velde]

import Mathlib.Algebra.Module.LinearMap.Basic

def LinearMap.neg (R : Type*) [Ring R] (A : Type*) [AddCommGroup A] [Module R A] : A →ₗ[R] A :=
  -LinearMap.id

theorem LinearMap.neg_apply' (R : Type*) [Ring R] (A : Type*) [AddCommGroup A] [Module R A] (x : A) :
    LinearMap.neg R A x = -x := rfl

[Eric Wieser]

docs#LinearEquiv.neg

[Ruben Van de Velde]

Or that!

[Kevin Buzzard]

Thanks both!