better home for inv_eq_zero?

Stream: general

[Abhimanyu Pallavi Sudhir]

When working on #801 I came across something really weird -- inv_eq_zero (which applies to discrete_field) is in data.real.nnreal. Isn't algebra.field a better place for it? Should I add this change to my PR or will it break a bunch of things?

I guess this is because inv_ne_zero is in init

[Chris Hughes]

It's probably because it applies to the division on nnreal, which is only a semifield or something.

[Abhimanyu Pallavi Sudhir]

They prove it for a discrete_field, then use it to prove it for nnreal with coercions. I don't see why it needs to be in the same file.

[Chris Hughes]

I see. That should be moved.

[Abhimanyu Pallavi Sudhir]

OK, I moved it to algebra.field in my PR.