x \diamond y = x^2 * y^-1 in SmallGroup(125,3) (the group of strictly upper triangular 3x3 matrices in F_5), as constructed in https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/FINITE.3A.20677.20-.3E.20255/near/490276270
Display order: elements are indexed 25a+5b+c via the normal form x = g1^a g2^b z^c, where g1, g2 generate the group and z = [g1,g2] generates the center. In these coordinates the operation is (a,b,c) \diamond (a',b',c') = (2a-a', 2b-b', 2c-c'-ab-a'b'+2a'b), so the table is the self-similar "2x-y mod 5" pattern at two nested scales (the 25x25 superblocks in a, the 5x5 blocks in b), with the central coordinate contributing the affine fine structure. [text written by Claude]
b-reinke · 2026-06-10 14:20:43
x \diamond y = x^2 * y^-1 in SmallGroup(125,3) (the group of strictly upper triangular 3x3 matrices in F_5), as constructed in https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/FINITE.3A.20677.20-.3E.20255/near/490276270
b-reinke · 2026-06-10 14:20:22
x \diamond y = x^2 * y^-1 in SmallGroup(125,3) (the group of strictly upper 3x3 matrices in F_5), as constructed in https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/FINITE.3A.20677.20-.3E.20255/near/490276270
dwrensha · 2026-06-12 17:15:50
b-reinke · 2026-06-10 14:20:43
b-reinke · 2026-06-10 14:20:22