algebra puzzle

Stream: maths

[Heather Macbeth]

Is this true?

import Mathlib
variable {R : Type*}

example [Semiring R] [IsLeftCancelAdd R] [IsRightCancelAdd R] [NoZeroDivisors R]
    {a b : R} (H : a ^ 2 + b ^ 2 = a * b + b * a) :
    a = b := by
  sorry

[Heather Macbeth]

Note that it is true over a ring (as opposed to a cancellative semiring):

example [Ring R] [NoZeroDivisors R]
    {a b : R} (H : a ^ 2 + b ^ 2 = a * b + b * a) :
    a = b := by
  have h : (a - b) ^ 2 = 0 := by linear_combination (norm := noncomm_ring) H
  linear_combination (norm := noncomm_ring) pow_eq_zero h

[Kyle Miller]

It seems not to be true, if I got this counterexample right:

Let $R\subseteq \mathbb{Z}[x]/(x^2)$ be the set of those $a+bx$ with either $a>0$ or $a=b=0$. This is a commutative semiring, and addition is cancellative since it is a sub-semiring of a ring. There are no zero divisors since $(a+bx)(c+dx)=0$ only if $ac=0$, which can only happen if $a=b=0$ or $c=d=0$.

With $a=1$ and $b=1+x$, we have $a^2+b^2=2+2x$ and $ab+ba=2+2x$, yet $a\neq b$.

So, NoZeroDivisors isn't inherited by the grothendieck completion of R.