How do I subtract endomorphisms?

Stream: new members

[Scott Carnahan]

I can't seem to use a minus sign when dealing with endomorphisms of a module - The computer assumes I want a heterogeneous subtraction.

import Mathlib.Algebra.Module.LinearMap

theorem sub_self_zero [CommRing R] [AddCommMonoid V] [Module R V] (f : Module.End R V) : f-f = 0 := sorry

Is this expected behavior?

[Patrick Massot]

What if you assume V itself has a negation? I mean use AddCommGroup V instead of AddCommMonoid V.

[Scott Carnahan]

Oh wow, it works! Thank you!

[Scott Carnahan]

(deleted)