I think youâ€™re misinterpreting what can merely be an example of the kind of equivalencies that â€śEq , Ord and Hash must be equivalent for borrowed and owned valuesâ€ť is supposed to imply, with the whole deal.

A more complete picture would, besides the already stated

(x == y) == (x.borrow() == y.borrow()),

also need to list

x.cmp(&y) == x.borrow().cmp(y.borrow()),

x.hash(&mut hasher) makes the same sequence of calls to hasher as x.borrow().hash(&mut hasher).

And furthermore it should probably need to qualify these conditions each by something like â€śif Self and Borrowed implements [Eq/Hash/Ord] correctlyâ€ť (which is supposed to mean both â€śif it implements the trait at allâ€ť, otherwise thereâ€™s no restriction, and furthermore doesnâ€™t blame consequences of logic errors from bad impls of Ord/Eq/Hash on the Borrow implementation^{[1]}).

No, this is wrong and (in general) doesnâ€™t even compile. x.borrow() has a different type from y. Itâ€™s not the values of x and x.borrow() (let alone y and x.borrow()) that must be the same, but just the behavior of corresponding values under trait operations that must be the same.

Mathematically, we are essentially specifying .borrow() to be somewhat of a homomorphism^{[1]}.

where L -> R is the sort of â€śimpliesâ€ť relation@drewtato wrote as if L { R } else { true } and one could also write as (!L) || R.

The consequence

x == y -> hash(x) == hash(y.borrow())

does follow from

hash(y) == hash(y.borrow())

and

x == y -> hash(x) == hash(y)

because in case of x == y being true, you can just chain equalities hash(x) == hash(y) == hash(y.borrow() to arrive at hash(x) == hash(y.borrow()) transitively.