Equalities, inequalities and fractions

Question

Today I was surprised by the following treatment of equations in Mathematica. I understand, for example, the following

In: a*b/a
Out: b

and nobody cares about what was the value of a. But I was quite surprised to find out that the same behavior takes place in case of equations. For example,

In: a*b/a!=0
Out: b!=0

I would expect the result a!=0&&b!=0 (or the original equation unchanged).

This leads to quite unexpected behavior in more complicated expressions. For example, if I wondered, whether there is a regular matrix of the form $A=\pmatrix{b/a&c\cr 0&a}$ such that $A\pmatrix{0\cr1}=\pmatrix{1\cr 0}$, I would write

In: Resolve[Exists[{a,b,c}, {{b/a,c},{0,a}}.{0,1}=={1,0} && Det[{{b/a,c},{0,a}}] != 0]]
Out: True

which surprisingly yields positive answer.

So, is this my bad programming? Should I put all equations into Reduce or something?

Answer 1

As explained in my answer to "How does FunctionDomain work?" question removable singularities are removed during ordinary evaluation of Times and Power functions. Since != (Unequal) has no evaluation holding Attributes, LHS of a*b/a != 0 expression evaluates to b before even Unequal "sees" it, so it can do nothing to pick out a != 0 condition.

Using RestrictDomain function from Domains` package, from already mentioned answer, we can add domain restricting conditions to any expression:

a*b/a // RestrictDomain
(* ConditionalExpression[b, a != 0] *)

a*b/a != 0 // RestrictDomain
(* ConditionalExpression[b != 0, a != 0] *)

Det[{{b/a, c}, {0, a}}] != 0 // RestrictDomain
(* ConditionalExpression[b != 0, a != 0] *)

Since Resolve can't handle ConditionalExpressions we need to convert them to logical sentences:

condExprToLogicSentence =
    # /. ConditionalExpression[expr_, cond_] :> expr && cond &;

Exists[{a, b, c},
    {{b/a, c}, {0, a}}.{0, 1} == {1, 0} && Det[{{b/a, c}, {0, a}}] != 0 //
    RestrictDomain // condExprToLogicSentence
]
(* Exists[{a, b, c}, {c, a} == {1, 0} && b != 0 && a != 0] *)
% // Resolve
(* False *)