Documentation

TauCeti.RepresentationTheory.CharacterTable.Dixon.Quaternion

Dixon prime data for the quaternion group of order eight #

The executable Dixon--Schneider algorithm receives a certified prime rather than searching for one noncomputably. This file certifies 5 for QuaternionGroup 2, together with 2 as a primitive fourth root of unity modulo 5.

Main definitions #

References #

source
theorem TauCeti.isGoodDixonPrime_quaternionGroup_two_five :
IsGoodDixonPrime (QuaternionGroup 2) 5

5 is a good Dixon prime for the quaternion group of order eight: 5 ∤ 8, its exponent 4 divides 5 - 1, and 2⌊√8⌋ = 4 < 5.

source
def TauCeti.quaternionGroupTwoDixonPrimeData :
DixonPrimeData (QuaternionGroup 2)

Dixon prime data for QuaternionGroup 2: the prime 5, with 2 as the primitive fourth root of unity modulo 5.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.quaternionGroupTwoDixonPrimeData_p :
    quaternionGroupTwoDixonPrimeData.p = 5

    The prime carried by TauCeti.quaternionGroupTwoDixonPrimeData is 5.

    source
    @[simp]
    theorem TauCeti.quaternionGroupTwoDixonPrimeData_root :
    quaternionGroupTwoDixonPrimeData.root = 2

    The primitive fourth root carried by TauCeti.quaternionGroupTwoDixonPrimeData is 2.