Post #1816236
2026-02-27 11:46 UTC
@de_Jong_Tom @MartinEscardo Thank you both for taking the time to write these much more readable formalisations. I like the idea of separately considering the consequences of commutativity and associativity on loops.
Replies (1)
-
@de_Jong_Tom@mathstodon.xyz 2026-02-27 12:10
@dwarn Here's a question that I can't answer: how did you come up with this?! Now that I've finished my file, I can explain the result and why it holds, but this is relatively easy because it's post-fact. It only worked because I knew it was true and could look up critical steps in your formalization. @MartinEscardo