Fix more errors spotted by @posco.

I changed the "generic multiplication" operator to make it harder
for people like me to get it mixed up with "generic addition".

I also removed the assumption that idempotence commutes. I'm not
sure it's true: if it is, we can modify it again later.