attribs.spad line 21 [edit on github]
The class of all semirings such that x * y ~= 0 implies both x and y are non-zero
x * y ~= 0
x
y