neg_zero for has_distrib_neg

Stream: Is there code for X?

[Eric Rodriguez]

do we have this somehwere already? else, should it be near the definition of docs#has_distrib_neg?

import algebra.algebra.basic

example {α} [mul_zero_class α] [has_distrib_neg α] : (-0 : α) = 0 :=
begin
  nth_rewrite 0 [←zero_mul (0 : α)],
  rw [←neg_mul, mul_zero]
end

[Eric Wieser]

Pretty sure that's missing, I didn't think of it when I wrote has_distrib_neg

[Eric Rodriguez]

#13049

[Eric Wieser]

Oh, the downside here is that this isn't just a generalization of docs#neg_zero

[Eric Wieser]

This is for your sign PR I assume?

[Yaël Dillies]

Soon, the has_neg_zero typeclass :rofl:

[Eric Rodriguez]

yeah, it's a shame :/ but yes, it is for sign