Newest at the top
| 2026-01-08 23:24:38 +0100 | AlexNoo | (~AlexNoo@178.34.163.50) |
| 2026-01-08 23:24:29 +0100 | <monochrom> | :) |
| 2026-01-08 23:24:16 +0100 | <Leary> | Actually the -0 could have been anything, should have just used 0. |
| 2026-01-08 23:23:11 +0100 | <tomsmeding> | so fully: 0 = -(a * -0) + a * -0 = -(a * -0) + a * (-0 + 0) = -(a * -0) + a * -0 + a * 0 = 0 + a * 0 = a * 0 |
| 2026-01-08 23:22:53 +0100 | <ncf> | Leary++ |
| 2026-01-08 23:21:59 +0100 | <Leary> | a * -0 = a * (-0 + 0) = a * -0 + a * 0 ==> a * 0 = 0 (by cancellation) |
| 2026-01-08 23:20:17 +0100 | <TMA> | the other order of operands need showing (-1)*a = a*(-1) |
| 2026-01-08 23:19:49 +0100 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 264 seconds) |
| 2026-01-08 23:19:47 +0100 | <Leary> | That still relies on `a * -1 = -a`. |
| 2026-01-08 23:19:38 +0100 | <tomsmeding> | oh also TMA :) |
| 2026-01-08 23:19:32 +0100 | <tomsmeding> | ncf: thank you |
| 2026-01-08 23:19:02 +0100 | <TMA> | 0*a = (x-x)*a = xa - xa = 0 for any x |
| 2026-01-08 23:18:47 +0100 | <ncf> | a * 0 = a * (1 - 1) = a - a = 0 ? |
| 2026-01-08 23:17:44 +0100 | <tomsmeding> | right, I just proved it in a long-winded way (see 6 minutes ago), but surely there's a more direct way |
| 2026-01-08 23:17:16 +0100 | <geekosaur> | but I think that's derived, not amxiom |
| 2026-01-08 23:17:06 +0100 | <tomsmeding> | geekosaur: no, because you can prove it so it need not be an axiom :p |
| 2026-01-08 23:16:51 +0100 | <monochrom> | Oh oops, sorry! Delete everything I said. |
| 2026-01-08 23:16:49 +0100 | <geekosaur> | 0 is required to be an annihilating element in multiplication |
| 2026-01-08 23:16:39 +0100 | xff0x | (~xff0x@2405:6580:b080:900:1a94:9136:5419:ce9c) (Ping timeout: 260 seconds) |
| 2026-01-08 23:16:34 +0100 | <tomsmeding> | this axiomatises 0 as the additive unit |
| 2026-01-08 23:16:32 +0100 | <geekosaur> | that was what I thought |
| 2026-01-08 23:16:27 +0100 | tomsmeding | is reading https://en.wikipedia.org/wiki/Ring_(mathematics) |
| 2026-01-08 23:16:26 +0100 | <monochrom> | To be sure I need a separate proof why it's unique. |
| 2026-01-08 23:16:13 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-08 23:16:10 +0100 | <monochrom> | 0 is axiomatized by "forall a, a*0 = 0". |
| 2026-01-08 23:15:30 +0100 | jmcantrell_ | jmcantrell |
| 2026-01-08 23:15:24 +0100 | <TMA> | tomsmeding: I have encountered ring definition containing the axiom 0!=1 as well |
| 2026-01-08 23:15:20 +0100 | tomsmeding | doesn't follow; doesn't that assume a*0 = 0 from the get go? |
| 2026-01-08 23:14:36 +0100 | <monochrom> | for all b, b*(a*0) = (b*a)*0 = 0. Then appeal to uniqueness of 0: "if forall b b*foo=0, then foo=0" |
| 2026-01-08 23:14:24 +0100 | xff0x_ | (~xff0x@2405:6580:b080:900:cd9:802b:8b60:b254) |
| 2026-01-08 23:11:33 +0100 | <tomsmeding> | (and 0 = a * 0 because: 0 = 1 + -1 = a * a^-1 + -1 = a * (0 + a^-1) + -1 = a * 0 + a * a^-1 + -1 = a * 0 + 1 + -1 = a * 0 + 0 = a * 0; there's probably a simpler derivation lol) |
| 2026-01-08 23:11:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-08 23:08:10 +0100 | <haskellbridge> | <loonycyborg> you can even divide by zero in this ring |
| 2026-01-08 23:07:12 +0100 | <tomsmeding> | if 1 = 0 then by the ring axioms, 0 = 0 * a = 1 * a = a, so all elements are zero, so it's the trivial ring, but it's allowed |
| 2026-01-08 23:06:49 +0100 | danz94513 | (~danza@user/danza) (Ping timeout: 246 seconds) |
| 2026-01-08 23:05:30 +0100 | <EvanR> | though we have good examples where they are, in crypto code |
| 2026-01-08 23:05:21 +0100 | <monochrom> | I agree. |
| 2026-01-08 23:04:37 +0100 | danza | (~danza@user/danza) danza |
| 2026-01-08 23:04:37 +0100 | <EvanR> | this whole time I was convinced that Num reflects a subcultural understanding of computer numbers and programmers are not usually thinking they're using a ring |
| 2026-01-08 23:04:32 +0100 | malte | (~malte@mal.tc) malte |
| 2026-01-08 23:04:26 +0100 | <geekosaur> | they're allowed to be the same… if there's only one value in the set |
| 2026-01-08 23:03:39 +0100 | <EvanR> | and a law saying they must be different? xD |
| 2026-01-08 23:03:31 +0100 | <EvanR> | zero and one |
| 2026-01-08 23:03:09 +0100 | malte | (~malte@mal.tc) (Ping timeout: 250 seconds) |
| 2026-01-08 23:00:58 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2026-01-08 23:00:43 +0100 | Googulator82 | Googulator |
| 2026-01-08 22:59:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-08 22:50:51 +0100 | <Leary> | monochrom: But sometimes that's the correct implementation. :) |
| 2026-01-08 22:50:25 +0100 | <monochrom> | You need a law to outlaw me trying "foldMap _ _ = mempty". |
| 2026-01-08 22:50:18 +0100 | <Leary> | Re `Num`, `abs` and `signum` should be moved to another class, and arguably `fromInteger` too (necessitating new `zero` and `one` methods). The rest could do to be split up or factored over `Monoid`, but it's otherwise fine and perfectly principled as a class for rings. |