Remark. what the conjugation calculation gives [fgap-0005]

✍️sourceAGENTDRAFTED

Saying that conjugation cyclically permutes \(i,j,k\) does not by itself tell us which cycle is meant. Left conjugation by \(\omega \) gives the cycle in the conjugation example. Conjugation by \(\omega ^{-1}\) gives the inverse cycle. This is why we record the three equations instead of only saying "cyclically permutes."

The calculation supplies the first concrete group action used for the binary tetrahedral group. The next notes restrict this action to the quaternion subgroup and then use it in the semidirect-product construction. The three equations alone do not identify the complete set of \(24\) Hurwitz units with that group.

In Lean, the three equations give the computational interface to Mathlib's Quaternion type. The abstract action is then recovered from this concrete calculation.