Eq(pi/L, 0) simplifies to False with L positive

[asmeurer]

>>> L = symbols("L", finite=True)
>>> Eq(pi/L, 0)
False
>>> L = symbols("L", positive=True)
>>> L.is_finite
>>> Eq(pi/L, 0)
False

If positive doesn't imply finite (we have oo.is_positive == True), then the second case shouldn't simplify.

[adityausathe]

@asmeurer
I am a newbie to the sympy world. I want to work on this one. Could you tell me what is the expected behaviour? Should Eq(pi/L, 0) evaluate to True?

[asmeurer]

It shouldn't simplify. L could be oo.

[BenediktEberhardinger]

I am also new and just started working on that issue by adding a test case that reproduces that bug.
I debugged the cause of the failure: it is in core.relational.py line 331 introduced by fixing #10728
The difference of pi/L and 0 is commutative and not zero thus False is returned.
From my point of view the fix to replace line 331 by
if z is False and not dif.is_complex:
I just wanted to double check with you, @asmeurer, whether that is correct.
If so, I could send a pull request to close that issue, if not, it would be great if you could give me a hint why False is returned when the difference is not zero and commutative.

[oscargus]

It seems like it does the right thing now anyway (as positive is finite now):

In [9]: L = symbols("L", finite=True)

In [10]: Eq(pi/L, 0)
Out[10]: False

In [11]: L = symbols("L", positive=True)

In [12]: Eq(pi/L, 0)
Out[12]: False

In [13]: L = symbols("L", extended_positive=True)

In [14]: Eq(pi/L, 0)
Out[14]: 
π    
─ = 0
L    

So I am closing.