neg as a linear map

Stream: Is there code for X?

[Sébastien Gouëzel]

I'm still lost in the maze of naming conventions for linear maps. What is the name of the linear map mapping x to -x in a module? I've found docs#IsLinearMap.isLinearMap_neg, which is almost this but not exactly. I'm missing a tool for which I would give the toFun field, and which would browse through all the definitions of linear maps we have to find me a map with this field.

[Yury G. Kudryashov]

Does -id work?

[Yury G. Kudryashov]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Module/LinearMap/Basic.html#LinearMap.instNegLinearMapToAddCommMonoid

[Eric Wieser]

docs#LinearEquiv.neg ?

[Yury G. Kudryashov]

Should we have Neg instance on LinearEquiv instead of LinearEquiv.neg?

[Eric Wieser]

@loogle LinearEquiv, Neg

[loogle]

:shrug: nothing found

[Eric Wieser]

Maybe? Though we can't do the same for docs#AddEquiv.neg'

[Eric Wieser]

So it would leave us with a primed name and no unprimed counterpart

[Sébastien Gouëzel]

For the record, in the end I used LinearIsometryEquiv.neg (which I found by redefining it and then getting a complaint from Lean that there was a name collision :-)

[Yury G. Kudryashov]

BTW, the docstring for docs#AddEquiv.neg' mentions AddEquiv.inv which doesn't exist.