Should has_neg be implied by mul_action?

Stream: new members

[Eric Wieser]

As in title. If I have mul_action A B and has_neg A, should lean provide has_neg B for me?

def neg (b : B) := smul (-1 : A) b

[Johan Commelin]

No, due to limitations in type class search, this is (unfortunately!) not possible. It should/might become better in Lean 4

[Johan Commelin]

So you will have to

def has_neg_of_mul_action : has_neg B := blabla

and then at the usage site

letI : has_neg B := has_neg_of_mul_action A B,

[Eric Wieser]

would has_neg_of_mul_action be a sensible addition to mathlib?

[Johan Commelin]

I guess so. Is there more structure around? Just a has_neg without information on how it interacts with other structure doesn't seem very useful.

[Eric Wieser]

Not really, it just seems awkward to be unable to write -b, and have to use (-1 : A) • b instead

[Scott Morrison]

What is the situation you're working in? It seems a bit strange if you have a has_neg A but no other structure.

[Eric Wieser]

I also have field A. What I meant was that B has little other structure.