HexConway.Bounds

source

theorem Hex.Conway.prime_two :

Nat.Prime 2

Primality of characteristic 2.

source

instance Hex.Conway.instPrimeModulus2 :

ZMod64.PrimeModulus 2

Prime modulus for characteristic 2.

source

instance Hex.Conway.bounds3 :

ZMod64.Bounds 3

Word bounds for characteristic 3.

source

theorem Hex.Conway.prime_three :

Nat.Prime 3

Primality of characteristic 3.

source

instance Hex.Conway.instPrimeModulus3 :

ZMod64.PrimeModulus 3

Prime modulus for characteristic 3.

source

instance Hex.Conway.bounds5 :

ZMod64.Bounds 5

Word bounds for characteristic 5.

source

theorem Hex.Conway.prime_five :

Nat.Prime 5

Primality of characteristic 5.

source

instance Hex.Conway.instPrimeModulus5 :

ZMod64.PrimeModulus 5

Prime modulus for characteristic 5.

source

instance Hex.Conway.bounds7 :

ZMod64.Bounds 7

Word bounds for characteristic 7.

source

theorem Hex.Conway.prime_seven :

Nat.Prime 7

Primality of characteristic 7.

source

instance Hex.Conway.instPrimeModulus7 :

ZMod64.PrimeModulus 7

Prime modulus for characteristic 7.

source

instance Hex.Conway.bounds11 :

ZMod64.Bounds 11

Word bounds for characteristic 11.

source

theorem Hex.Conway.prime_eleven :

Nat.Prime 11

Primality of characteristic 11.

source

instance Hex.Conway.instPrimeModulus11 :

ZMod64.PrimeModulus 11

Prime modulus for characteristic 11.

source

instance Hex.Conway.bounds13 :

ZMod64.Bounds 13

Word bounds for characteristic 13.

source

theorem Hex.Conway.prime_thirteen :

Nat.Prime 13

Primality of characteristic 13.

source

instance Hex.Conway.instPrimeModulus13 :

ZMod64.PrimeModulus 13

Prime modulus for characteristic 13.

source

instance Hex.Conway.bounds17 :

ZMod64.Bounds 17

Word bounds for characteristic 17.

source

theorem Hex.Conway.prime_17 :

Nat.Prime 17

Primality of characteristic 17.

source

instance Hex.Conway.instPrimeModulus17 :

ZMod64.PrimeModulus 17

Prime modulus for characteristic 17.

source

instance Hex.Conway.bounds19 :

ZMod64.Bounds 19

Word bounds for characteristic 19.

source

theorem Hex.Conway.prime_19 :

Nat.Prime 19

Primality of characteristic 19.

source

instance Hex.Conway.instPrimeModulus19 :

ZMod64.PrimeModulus 19

Prime modulus for characteristic 19.

source

instance Hex.Conway.bounds23 :

ZMod64.Bounds 23

Word bounds for characteristic 23.

source

theorem Hex.Conway.prime_23 :

Nat.Prime 23

Primality of characteristic 23.

source

instance Hex.Conway.instPrimeModulus23 :

ZMod64.PrimeModulus 23

Prime modulus for characteristic 23.

source

instance Hex.Conway.bounds29 :

ZMod64.Bounds 29

Word bounds for characteristic 29.

source

theorem Hex.Conway.prime_29 :

Nat.Prime 29

Primality of characteristic 29.

source

instance Hex.Conway.instPrimeModulus29 :

ZMod64.PrimeModulus 29

Prime modulus for characteristic 29.

source

instance Hex.Conway.bounds31 :

ZMod64.Bounds 31

Word bounds for characteristic 31.

source

theorem Hex.Conway.prime_31 :

Nat.Prime 31

Primality of characteristic 31.

source

instance Hex.Conway.instPrimeModulus31 :

ZMod64.PrimeModulus 31

Prime modulus for characteristic 31.

source

instance Hex.Conway.bounds37 :

ZMod64.Bounds 37

Word bounds for characteristic 37.

source

theorem Hex.Conway.prime_37 :

Nat.Prime 37

Primality of characteristic 37.

source

instance Hex.Conway.instPrimeModulus37 :

ZMod64.PrimeModulus 37

Prime modulus for characteristic 37.

source

instance Hex.Conway.bounds41 :

ZMod64.Bounds 41

Word bounds for characteristic 41.

source

theorem Hex.Conway.prime_41 :

Nat.Prime 41

Primality of characteristic 41.

source

instance Hex.Conway.instPrimeModulus41 :

ZMod64.PrimeModulus 41

Prime modulus for characteristic 41.

source

instance Hex.Conway.bounds43 :

ZMod64.Bounds 43

Word bounds for characteristic 43.

source

theorem Hex.Conway.prime_43 :

Nat.Prime 43

Primality of characteristic 43.

source

instance Hex.Conway.instPrimeModulus43 :

ZMod64.PrimeModulus 43

Prime modulus for characteristic 43.

source

instance Hex.Conway.bounds47 :

ZMod64.Bounds 47

Word bounds for characteristic 47.

source

theorem Hex.Conway.prime_47 :

Nat.Prime 47

Primality of characteristic 47.

source

instance Hex.Conway.instPrimeModulus47 :

ZMod64.PrimeModulus 47

Prime modulus for characteristic 47.

source

instance Hex.Conway.bounds53 :

ZMod64.Bounds 53

Word bounds for characteristic 53.

source

theorem Hex.Conway.prime_53 :

Nat.Prime 53

Primality of characteristic 53.

source

instance Hex.Conway.instPrimeModulus53 :

ZMod64.PrimeModulus 53

Prime modulus for characteristic 53.

source

instance Hex.Conway.bounds59 :

ZMod64.Bounds 59

Word bounds for characteristic 59.

source

theorem Hex.Conway.prime_59 :

Nat.Prime 59

Primality of characteristic 59.

source

instance Hex.Conway.instPrimeModulus59 :

ZMod64.PrimeModulus 59

Prime modulus for characteristic 59.

source

instance Hex.Conway.bounds61 :

ZMod64.Bounds 61

Word bounds for characteristic 61.

source

theorem Hex.Conway.prime_61 :

Nat.Prime 61

Primality of characteristic 61.

source

instance Hex.Conway.instPrimeModulus61 :

ZMod64.PrimeModulus 61

Prime modulus for characteristic 61.

source

instance Hex.Conway.bounds67 :

ZMod64.Bounds 67

Word bounds for characteristic 67.

source

theorem Hex.Conway.prime_67 :

Nat.Prime 67

Primality of characteristic 67.

source

instance Hex.Conway.instPrimeModulus67 :

ZMod64.PrimeModulus 67

Prime modulus for characteristic 67.

source

instance Hex.Conway.bounds71 :

ZMod64.Bounds 71

Word bounds for characteristic 71.

source

theorem Hex.Conway.prime_71 :

Nat.Prime 71

Primality of characteristic 71.

source

instance Hex.Conway.instPrimeModulus71 :

ZMod64.PrimeModulus 71

Prime modulus for characteristic 71.

source

instance Hex.Conway.bounds73 :

ZMod64.Bounds 73

Word bounds for characteristic 73.

source

theorem Hex.Conway.prime_73 :

Nat.Prime 73

Primality of characteristic 73.

source

instance Hex.Conway.instPrimeModulus73 :

ZMod64.PrimeModulus 73

Prime modulus for characteristic 73.

source

instance Hex.Conway.bounds79 :

ZMod64.Bounds 79

Word bounds for characteristic 79.

source

theorem Hex.Conway.prime_79 :

Nat.Prime 79

Primality of characteristic 79.

source

instance Hex.Conway.instPrimeModulus79 :

ZMod64.PrimeModulus 79

Prime modulus for characteristic 79.

source

instance Hex.Conway.bounds83 :

ZMod64.Bounds 83

Word bounds for characteristic 83.

source

theorem Hex.Conway.prime_83 :

Nat.Prime 83

Primality of characteristic 83.

source

instance Hex.Conway.instPrimeModulus83 :

ZMod64.PrimeModulus 83

Prime modulus for characteristic 83.

source

instance Hex.Conway.bounds89 :

ZMod64.Bounds 89

Word bounds for characteristic 89.

source

theorem Hex.Conway.prime_89 :

Nat.Prime 89

Primality of characteristic 89.

source

instance Hex.Conway.instPrimeModulus89 :

ZMod64.PrimeModulus 89

Prime modulus for characteristic 89.

source

instance Hex.Conway.bounds97 :

ZMod64.Bounds 97

Word bounds for characteristic 97.

source

theorem Hex.Conway.prime_97 :

Nat.Prime 97

Primality of characteristic 97.

source

instance Hex.Conway.instPrimeModulus97 :

ZMod64.PrimeModulus 97

Prime modulus for characteristic 97.

source

instance Hex.Conway.bounds101 :

ZMod64.Bounds 101

Word bounds for characteristic 101.

source

theorem Hex.Conway.prime_101 :

Nat.Prime 101

Primality of characteristic 101.

source

instance Hex.Conway.instPrimeModulus101 :

ZMod64.PrimeModulus 101

Prime modulus for characteristic 101.

source

instance Hex.Conway.bounds103 :

ZMod64.Bounds 103

Word bounds for characteristic 103.

source

theorem Hex.Conway.prime_103 :

Nat.Prime 103

Primality of characteristic 103.

source

instance Hex.Conway.instPrimeModulus103 :

ZMod64.PrimeModulus 103

Prime modulus for characteristic 103.

source

instance Hex.Conway.bounds107 :

ZMod64.Bounds 107

Word bounds for characteristic 107.

source

theorem Hex.Conway.prime_107 :

Nat.Prime 107

Primality of characteristic 107.

source

instance Hex.Conway.instPrimeModulus107 :

ZMod64.PrimeModulus 107

Prime modulus for characteristic 107.

source

instance Hex.Conway.bounds109 :

ZMod64.Bounds 109

Word bounds for characteristic 109.

source

theorem Hex.Conway.prime_109 :

Nat.Prime 109

Primality of characteristic 109.

source

instance Hex.Conway.instPrimeModulus109 :

ZMod64.PrimeModulus 109

Prime modulus for characteristic 109.

source

instance Hex.Conway.bounds113 :

ZMod64.Bounds 113

Word bounds for characteristic 113.

source

theorem Hex.Conway.prime_113 :

Nat.Prime 113

Primality of characteristic 113.

source

instance Hex.Conway.instPrimeModulus113 :

ZMod64.PrimeModulus 113

Prime modulus for characteristic 113.

source

instance Hex.Conway.bounds127 :

ZMod64.Bounds 127

Word bounds for characteristic 127.

source

theorem Hex.Conway.prime_127 :

Nat.Prime 127

Primality of characteristic 127.

source

instance Hex.Conway.instPrimeModulus127 :

ZMod64.PrimeModulus 127

Prime modulus for characteristic 127.

source

instance Hex.Conway.bounds131 :

ZMod64.Bounds 131

Word bounds for characteristic 131.

source

theorem Hex.Conway.prime_131 :

Nat.Prime 131

Primality of characteristic 131.

source

instance Hex.Conway.instPrimeModulus131 :

ZMod64.PrimeModulus 131

Prime modulus for characteristic 131.

source

instance Hex.Conway.bounds137 :

ZMod64.Bounds 137

Word bounds for characteristic 137.

source

theorem Hex.Conway.prime_137 :

Nat.Prime 137

Primality of characteristic 137.

source

instance Hex.Conway.instPrimeModulus137 :

ZMod64.PrimeModulus 137

Prime modulus for characteristic 137.

source

instance Hex.Conway.bounds139 :

ZMod64.Bounds 139

Word bounds for characteristic 139.

source

theorem Hex.Conway.prime_139 :

Nat.Prime 139

Primality of characteristic 139.

source

instance Hex.Conway.instPrimeModulus139 :

ZMod64.PrimeModulus 139

Prime modulus for characteristic 139.

source

instance Hex.Conway.bounds149 :

ZMod64.Bounds 149

Word bounds for characteristic 149.

source

theorem Hex.Conway.prime_149 :

Nat.Prime 149

Primality of characteristic 149.

source

instance Hex.Conway.instPrimeModulus149 :

ZMod64.PrimeModulus 149

Prime modulus for characteristic 149.

source

instance Hex.Conway.bounds151 :

ZMod64.Bounds 151

Word bounds for characteristic 151.

source

theorem Hex.Conway.prime_151 :

Nat.Prime 151

Primality of characteristic 151.

source

instance Hex.Conway.instPrimeModulus151 :

ZMod64.PrimeModulus 151

Prime modulus for characteristic 151.

source

instance Hex.Conway.bounds157 :

ZMod64.Bounds 157

Word bounds for characteristic 157.

source

theorem Hex.Conway.prime_157 :

Nat.Prime 157

Primality of characteristic 157.

source

instance Hex.Conway.instPrimeModulus157 :

ZMod64.PrimeModulus 157

Prime modulus for characteristic 157.

source

instance Hex.Conway.bounds163 :

ZMod64.Bounds 163

Word bounds for characteristic 163.

source

theorem Hex.Conway.prime_163 :

Nat.Prime 163

Primality of characteristic 163.

source

instance Hex.Conway.instPrimeModulus163 :

ZMod64.PrimeModulus 163

Prime modulus for characteristic 163.

source

instance Hex.Conway.bounds167 :

ZMod64.Bounds 167

Word bounds for characteristic 167.

source

theorem Hex.Conway.prime_167 :

Nat.Prime 167

Primality of characteristic 167.

source

instance Hex.Conway.instPrimeModulus167 :

ZMod64.PrimeModulus 167

Prime modulus for characteristic 167.

source

instance Hex.Conway.bounds173 :

ZMod64.Bounds 173

Word bounds for characteristic 173.

source

theorem Hex.Conway.prime_173 :

Nat.Prime 173

Primality of characteristic 173.

source

instance Hex.Conway.instPrimeModulus173 :

ZMod64.PrimeModulus 173

Prime modulus for characteristic 173.

source

instance Hex.Conway.bounds179 :

ZMod64.Bounds 179

Word bounds for characteristic 179.

source

theorem Hex.Conway.prime_179 :

Nat.Prime 179

Primality of characteristic 179.

source

instance Hex.Conway.instPrimeModulus179 :

ZMod64.PrimeModulus 179

Prime modulus for characteristic 179.

source

instance Hex.Conway.bounds181 :

ZMod64.Bounds 181

Word bounds for characteristic 181.

source

theorem Hex.Conway.prime_181 :

Nat.Prime 181

Primality of characteristic 181.

source

instance Hex.Conway.instPrimeModulus181 :

ZMod64.PrimeModulus 181

Prime modulus for characteristic 181.

source

instance Hex.Conway.bounds191 :

ZMod64.Bounds 191

Word bounds for characteristic 191.

source

theorem Hex.Conway.prime_191 :

Nat.Prime 191

Primality of characteristic 191.

source

instance Hex.Conway.instPrimeModulus191 :

ZMod64.PrimeModulus 191

Prime modulus for characteristic 191.

source

instance Hex.Conway.bounds193 :

ZMod64.Bounds 193

Word bounds for characteristic 193.

source

theorem Hex.Conway.prime_193 :

Nat.Prime 193

Primality of characteristic 193.

source

instance Hex.Conway.instPrimeModulus193 :

ZMod64.PrimeModulus 193

Prime modulus for characteristic 193.

source

instance Hex.Conway.bounds197 :

ZMod64.Bounds 197

Word bounds for characteristic 197.

source

theorem Hex.Conway.prime_197 :

Nat.Prime 197

Primality of characteristic 197.

source

instance Hex.Conway.instPrimeModulus197 :

ZMod64.PrimeModulus 197

Prime modulus for characteristic 197.

source

instance Hex.Conway.bounds199 :

ZMod64.Bounds 199

Word bounds for characteristic 199.

source

theorem Hex.Conway.prime_199 :

Nat.Prime 199

Primality of characteristic 199.

source

instance Hex.Conway.instPrimeModulus199 :

ZMod64.PrimeModulus 199

Prime modulus for characteristic 199.

source

instance Hex.Conway.bounds211 :

ZMod64.Bounds 211

Word bounds for characteristic 211.

source

theorem Hex.Conway.prime_211 :

Nat.Prime 211

Primality of characteristic 211.

source

instance Hex.Conway.instPrimeModulus211 :

ZMod64.PrimeModulus 211

Prime modulus for characteristic 211.

source

instance Hex.Conway.bounds223 :

ZMod64.Bounds 223

Word bounds for characteristic 223.

source

theorem Hex.Conway.prime_223 :

Nat.Prime 223

Primality of characteristic 223.

source

instance Hex.Conway.instPrimeModulus223 :

ZMod64.PrimeModulus 223

Prime modulus for characteristic 223.

source

instance Hex.Conway.bounds227 :

ZMod64.Bounds 227

Word bounds for characteristic 227.

source

theorem Hex.Conway.prime_227 :

Nat.Prime 227

Primality of characteristic 227.

source

instance Hex.Conway.instPrimeModulus227 :

ZMod64.PrimeModulus 227

Prime modulus for characteristic 227.

source

instance Hex.Conway.bounds229 :

ZMod64.Bounds 229

Word bounds for characteristic 229.

source

theorem Hex.Conway.prime_229 :

Nat.Prime 229

Primality of characteristic 229.

source

instance Hex.Conway.instPrimeModulus229 :

ZMod64.PrimeModulus 229

Prime modulus for characteristic 229.

source

instance Hex.Conway.bounds233 :

ZMod64.Bounds 233

Word bounds for characteristic 233.

source

theorem Hex.Conway.prime_233 :

Nat.Prime 233

Primality of characteristic 233.

source

instance Hex.Conway.instPrimeModulus233 :

ZMod64.PrimeModulus 233

Prime modulus for characteristic 233.

source

instance Hex.Conway.bounds239 :

ZMod64.Bounds 239

Word bounds for characteristic 239.

source

theorem Hex.Conway.prime_239 :

Nat.Prime 239

Primality of characteristic 239.

source

instance Hex.Conway.instPrimeModulus239 :

ZMod64.PrimeModulus 239

Prime modulus for characteristic 239.

source

instance Hex.Conway.bounds241 :

ZMod64.Bounds 241

Word bounds for characteristic 241.

source

theorem Hex.Conway.prime_241 :

Nat.Prime 241

Primality of characteristic 241.

source

instance Hex.Conway.instPrimeModulus241 :

ZMod64.PrimeModulus 241

Prime modulus for characteristic 241.

source

instance Hex.Conway.bounds251 :

ZMod64.Bounds 251

Word bounds for characteristic 251.

source

theorem Hex.Conway.prime_251 :

Nat.Prime 251

Primality of characteristic 251.

source

instance Hex.Conway.instPrimeModulus251 :

ZMod64.PrimeModulus 251

Prime modulus for characteristic 251.

source

instance Hex.Conway.bounds257 :

ZMod64.Bounds 257

Word bounds for characteristic 257.

source

theorem Hex.Conway.prime_257 :

Nat.Prime 257

Primality of characteristic 257.

source

instance Hex.Conway.instPrimeModulus257 :

ZMod64.PrimeModulus 257

Prime modulus for characteristic 257.

source

instance Hex.Conway.bounds263 :

ZMod64.Bounds 263

Word bounds for characteristic 263.

source

theorem Hex.Conway.prime_263 :

Nat.Prime 263

Primality of characteristic 263.

source

instance Hex.Conway.instPrimeModulus263 :

ZMod64.PrimeModulus 263

Prime modulus for characteristic 263.

source

instance Hex.Conway.bounds269 :

ZMod64.Bounds 269

Word bounds for characteristic 269.

source

theorem Hex.Conway.prime_269 :

Nat.Prime 269

Primality of characteristic 269.

source

instance Hex.Conway.instPrimeModulus269 :

ZMod64.PrimeModulus 269

Prime modulus for characteristic 269.

source

instance Hex.Conway.bounds271 :

ZMod64.Bounds 271

Word bounds for characteristic 271.

source

theorem Hex.Conway.prime_271 :

Nat.Prime 271

Primality of characteristic 271.

source

instance Hex.Conway.instPrimeModulus271 :

ZMod64.PrimeModulus 271

Prime modulus for characteristic 271.

source

instance Hex.Conway.bounds277 :

ZMod64.Bounds 277

Word bounds for characteristic 277.

source

theorem Hex.Conway.prime_277 :

Nat.Prime 277

Primality of characteristic 277.

source

instance Hex.Conway.instPrimeModulus277 :

ZMod64.PrimeModulus 277

Prime modulus for characteristic 277.

source

instance Hex.Conway.bounds281 :

ZMod64.Bounds 281

Word bounds for characteristic 281.

source

theorem Hex.Conway.prime_281 :

Nat.Prime 281

Primality of characteristic 281.

source

instance Hex.Conway.instPrimeModulus281 :

ZMod64.PrimeModulus 281

Prime modulus for characteristic 281.

source

instance Hex.Conway.bounds283 :

ZMod64.Bounds 283

Word bounds for characteristic 283.

source

theorem Hex.Conway.prime_283 :

Nat.Prime 283

Primality of characteristic 283.

source

instance Hex.Conway.instPrimeModulus283 :

ZMod64.PrimeModulus 283

Prime modulus for characteristic 283.

source

instance Hex.Conway.bounds293 :

ZMod64.Bounds 293

Word bounds for characteristic 293.

source

theorem Hex.Conway.prime_293 :

Nat.Prime 293

Primality of characteristic 293.

source

instance Hex.Conway.instPrimeModulus293 :

ZMod64.PrimeModulus 293

Prime modulus for characteristic 293.

source

instance Hex.Conway.bounds307 :

ZMod64.Bounds 307

Word bounds for characteristic 307.

source

theorem Hex.Conway.prime_307 :

Nat.Prime 307

Primality of characteristic 307.

source

instance Hex.Conway.instPrimeModulus307 :

ZMod64.PrimeModulus 307

Prime modulus for characteristic 307.

source

instance Hex.Conway.bounds311 :

ZMod64.Bounds 311

Word bounds for characteristic 311.

source

theorem Hex.Conway.prime_311 :

Nat.Prime 311

Primality of characteristic 311.

source

instance Hex.Conway.instPrimeModulus311 :

ZMod64.PrimeModulus 311

Prime modulus for characteristic 311.

source

instance Hex.Conway.bounds313 :

ZMod64.Bounds 313

Word bounds for characteristic 313.

source

theorem Hex.Conway.prime_313 :

Nat.Prime 313

Primality of characteristic 313.

source

instance Hex.Conway.instPrimeModulus313 :

ZMod64.PrimeModulus 313

Prime modulus for characteristic 313.

source

instance Hex.Conway.bounds317 :

ZMod64.Bounds 317

Word bounds for characteristic 317.

source

theorem Hex.Conway.prime_317 :

Nat.Prime 317

Primality of characteristic 317.

source

instance Hex.Conway.instPrimeModulus317 :

ZMod64.PrimeModulus 317

Prime modulus for characteristic 317.

source

instance Hex.Conway.bounds331 :

ZMod64.Bounds 331

Word bounds for characteristic 331.

source

theorem Hex.Conway.prime_331 :

Nat.Prime 331

Primality of characteristic 331.

source

instance Hex.Conway.instPrimeModulus331 :

ZMod64.PrimeModulus 331

Prime modulus for characteristic 331.

source

instance Hex.Conway.bounds337 :

ZMod64.Bounds 337

Word bounds for characteristic 337.

source

theorem Hex.Conway.prime_337 :

Nat.Prime 337

Primality of characteristic 337.

source

instance Hex.Conway.instPrimeModulus337 :

ZMod64.PrimeModulus 337

Prime modulus for characteristic 337.

source

instance Hex.Conway.bounds347 :

ZMod64.Bounds 347

Word bounds for characteristic 347.

source

theorem Hex.Conway.prime_347 :

Nat.Prime 347

Primality of characteristic 347.

source

instance Hex.Conway.instPrimeModulus347 :

ZMod64.PrimeModulus 347

Prime modulus for characteristic 347.

source

instance Hex.Conway.bounds349 :

ZMod64.Bounds 349

Word bounds for characteristic 349.

source

theorem Hex.Conway.prime_349 :

Nat.Prime 349

Primality of characteristic 349.

source

instance Hex.Conway.instPrimeModulus349 :

ZMod64.PrimeModulus 349

Prime modulus for characteristic 349.

source

instance Hex.Conway.bounds353 :

ZMod64.Bounds 353

Word bounds for characteristic 353.

source

theorem Hex.Conway.prime_353 :

Nat.Prime 353

Primality of characteristic 353.

source

instance Hex.Conway.instPrimeModulus353 :

ZMod64.PrimeModulus 353

Prime modulus for characteristic 353.

source

instance Hex.Conway.bounds359 :

ZMod64.Bounds 359

Word bounds for characteristic 359.

source

theorem Hex.Conway.prime_359 :

Nat.Prime 359

Primality of characteristic 359.

source

instance Hex.Conway.instPrimeModulus359 :

ZMod64.PrimeModulus 359

Prime modulus for characteristic 359.

source

instance Hex.Conway.bounds367 :

ZMod64.Bounds 367

Word bounds for characteristic 367.

source

theorem Hex.Conway.prime_367 :

Nat.Prime 367

Primality of characteristic 367.

source

instance Hex.Conway.instPrimeModulus367 :

ZMod64.PrimeModulus 367

Prime modulus for characteristic 367.

source

instance Hex.Conway.bounds373 :

ZMod64.Bounds 373

Word bounds for characteristic 373.

source

theorem Hex.Conway.prime_373 :

Nat.Prime 373

Primality of characteristic 373.

source

instance Hex.Conway.instPrimeModulus373 :

ZMod64.PrimeModulus 373

Prime modulus for characteristic 373.

source

instance Hex.Conway.bounds379 :

ZMod64.Bounds 379

Word bounds for characteristic 379.

source

theorem Hex.Conway.prime_379 :

Nat.Prime 379

Primality of characteristic 379.

source

instance Hex.Conway.instPrimeModulus379 :

ZMod64.PrimeModulus 379

Prime modulus for characteristic 379.

source

instance Hex.Conway.bounds383 :

ZMod64.Bounds 383

Word bounds for characteristic 383.

source

theorem Hex.Conway.prime_383 :

Nat.Prime 383

Primality of characteristic 383.

source

instance Hex.Conway.instPrimeModulus383 :

ZMod64.PrimeModulus 383

Prime modulus for characteristic 383.

source

instance Hex.Conway.bounds389 :

ZMod64.Bounds 389

Word bounds for characteristic 389.

source

theorem Hex.Conway.prime_389 :

Nat.Prime 389

Primality of characteristic 389.

source

instance Hex.Conway.instPrimeModulus389 :

ZMod64.PrimeModulus 389

Prime modulus for characteristic 389.

source

instance Hex.Conway.bounds397 :

ZMod64.Bounds 397

Word bounds for characteristic 397.

source

theorem Hex.Conway.prime_397 :

Nat.Prime 397

Primality of characteristic 397.

source

instance Hex.Conway.instPrimeModulus397 :

ZMod64.PrimeModulus 397

Prime modulus for characteristic 397.

source

instance Hex.Conway.bounds401 :

ZMod64.Bounds 401

Word bounds for characteristic 401.

source

theorem Hex.Conway.prime_401 :

Nat.Prime 401

Primality of characteristic 401.

source

instance Hex.Conway.instPrimeModulus401 :

ZMod64.PrimeModulus 401

Prime modulus for characteristic 401.

source

instance Hex.Conway.bounds409 :

ZMod64.Bounds 409

Word bounds for characteristic 409.

source

theorem Hex.Conway.prime_409 :

Nat.Prime 409

Primality of characteristic 409.

source

instance Hex.Conway.instPrimeModulus409 :

ZMod64.PrimeModulus 409

Prime modulus for characteristic 409.

source

instance Hex.Conway.bounds419 :

ZMod64.Bounds 419

Word bounds for characteristic 419.

source

theorem Hex.Conway.prime_419 :

Nat.Prime 419

Primality of characteristic 419.

source

instance Hex.Conway.instPrimeModulus419 :

ZMod64.PrimeModulus 419

Prime modulus for characteristic 419.

source

instance Hex.Conway.bounds421 :

ZMod64.Bounds 421

Word bounds for characteristic 421.

source

theorem Hex.Conway.prime_421 :

Nat.Prime 421

Primality of characteristic 421.

source

instance Hex.Conway.instPrimeModulus421 :

ZMod64.PrimeModulus 421

Prime modulus for characteristic 421.

source

instance Hex.Conway.bounds431 :

ZMod64.Bounds 431

Word bounds for characteristic 431.

source

theorem Hex.Conway.prime_431 :

Nat.Prime 431

Primality of characteristic 431.

source

instance Hex.Conway.instPrimeModulus431 :

ZMod64.PrimeModulus 431

Prime modulus for characteristic 431.

source

instance Hex.Conway.bounds433 :

ZMod64.Bounds 433

Word bounds for characteristic 433.

source

theorem Hex.Conway.prime_433 :

Nat.Prime 433

Primality of characteristic 433.

source

instance Hex.Conway.instPrimeModulus433 :

ZMod64.PrimeModulus 433

Prime modulus for characteristic 433.

source

instance Hex.Conway.bounds439 :

ZMod64.Bounds 439

Word bounds for characteristic 439.

source

theorem Hex.Conway.prime_439 :

Nat.Prime 439

Primality of characteristic 439.

source

instance Hex.Conway.instPrimeModulus439 :

ZMod64.PrimeModulus 439

Prime modulus for characteristic 439.

source

instance Hex.Conway.bounds443 :

ZMod64.Bounds 443

Word bounds for characteristic 443.

source

theorem Hex.Conway.prime_443 :

Nat.Prime 443

Primality of characteristic 443.

source

instance Hex.Conway.instPrimeModulus443 :

ZMod64.PrimeModulus 443

Prime modulus for characteristic 443.

source

instance Hex.Conway.bounds449 :

ZMod64.Bounds 449

Word bounds for characteristic 449.

source

theorem Hex.Conway.prime_449 :

Nat.Prime 449

Primality of characteristic 449.

source

instance Hex.Conway.instPrimeModulus449 :

ZMod64.PrimeModulus 449

Prime modulus for characteristic 449.

source

instance Hex.Conway.bounds457 :

ZMod64.Bounds 457

Word bounds for characteristic 457.

source

theorem Hex.Conway.prime_457 :

Nat.Prime 457

Primality of characteristic 457.

source

instance Hex.Conway.instPrimeModulus457 :

ZMod64.PrimeModulus 457

Prime modulus for characteristic 457.

source

instance Hex.Conway.bounds461 :

ZMod64.Bounds 461

Word bounds for characteristic 461.

source

theorem Hex.Conway.prime_461 :

Nat.Prime 461

Primality of characteristic 461.

source

instance Hex.Conway.instPrimeModulus461 :

ZMod64.PrimeModulus 461

Prime modulus for characteristic 461.

source

instance Hex.Conway.bounds463 :

ZMod64.Bounds 463

Word bounds for characteristic 463.

source

theorem Hex.Conway.prime_463 :

Nat.Prime 463

Primality of characteristic 463.

source

instance Hex.Conway.instPrimeModulus463 :

ZMod64.PrimeModulus 463

Prime modulus for characteristic 463.

source

instance Hex.Conway.bounds467 :

ZMod64.Bounds 467

Word bounds for characteristic 467.

source

theorem Hex.Conway.prime_467 :

Nat.Prime 467

Primality of characteristic 467.

source

instance Hex.Conway.instPrimeModulus467 :

ZMod64.PrimeModulus 467

Prime modulus for characteristic 467.

source

instance Hex.Conway.bounds479 :

ZMod64.Bounds 479

Word bounds for characteristic 479.

source

theorem Hex.Conway.prime_479 :

Nat.Prime 479

Primality of characteristic 479.

source

instance Hex.Conway.instPrimeModulus479 :

ZMod64.PrimeModulus 479

Prime modulus for characteristic 479.

source

instance Hex.Conway.bounds487 :

ZMod64.Bounds 487

Word bounds for characteristic 487.

source

theorem Hex.Conway.prime_487 :

Nat.Prime 487

Primality of characteristic 487.

source

instance Hex.Conway.instPrimeModulus487 :

ZMod64.PrimeModulus 487

Prime modulus for characteristic 487.

source

instance Hex.Conway.bounds491 :

ZMod64.Bounds 491

Word bounds for characteristic 491.

source

theorem Hex.Conway.prime_491 :

Nat.Prime 491

Primality of characteristic 491.

source

instance Hex.Conway.instPrimeModulus491 :

ZMod64.PrimeModulus 491

Prime modulus for characteristic 491.

source

instance Hex.Conway.bounds499 :

ZMod64.Bounds 499

Word bounds for characteristic 499.

source

theorem Hex.Conway.prime_499 :

Nat.Prime 499

Primality of characteristic 499.

source

instance Hex.Conway.instPrimeModulus499 :

ZMod64.PrimeModulus 499

Prime modulus for characteristic 499.

source

instance Hex.Conway.bounds503 :

ZMod64.Bounds 503

Word bounds for characteristic 503.

source

theorem Hex.Conway.prime_503 :

Nat.Prime 503

Primality of characteristic 503.

source

instance Hex.Conway.instPrimeModulus503 :

ZMod64.PrimeModulus 503

Prime modulus for characteristic 503.

source

instance Hex.Conway.bounds509 :

ZMod64.Bounds 509

Word bounds for characteristic 509.

source

theorem Hex.Conway.prime_509 :

Nat.Prime 509

Primality of characteristic 509.

source

instance Hex.Conway.instPrimeModulus509 :

ZMod64.PrimeModulus 509

Prime modulus for characteristic 509.

source

instance Hex.Conway.bounds521 :

ZMod64.Bounds 521

Word bounds for characteristic 521.

source

theorem Hex.Conway.prime_521 :

Nat.Prime 521

Primality of characteristic 521.

source

instance Hex.Conway.instPrimeModulus521 :

ZMod64.PrimeModulus 521

Prime modulus for characteristic 521.

source

instance Hex.Conway.bounds523 :

ZMod64.Bounds 523

Word bounds for characteristic 523.

source

theorem Hex.Conway.prime_523 :

Nat.Prime 523

Primality of characteristic 523.

source

instance Hex.Conway.instPrimeModulus523 :

ZMod64.PrimeModulus 523

Prime modulus for characteristic 523.

source

instance Hex.Conway.bounds541 :

ZMod64.Bounds 541

Word bounds for characteristic 541.

source

theorem Hex.Conway.prime_541 :

Nat.Prime 541

Primality of characteristic 541.

source

instance Hex.Conway.instPrimeModulus541 :

ZMod64.PrimeModulus 541

Prime modulus for characteristic 541.

source

instance Hex.Conway.bounds547 :

ZMod64.Bounds 547

Word bounds for characteristic 547.

source

theorem Hex.Conway.prime_547 :

Nat.Prime 547

Primality of characteristic 547.

source

instance Hex.Conway.instPrimeModulus547 :

ZMod64.PrimeModulus 547

Prime modulus for characteristic 547.

source

instance Hex.Conway.bounds557 :

ZMod64.Bounds 557

Word bounds for characteristic 557.

source

theorem Hex.Conway.prime_557 :

Nat.Prime 557

Primality of characteristic 557.

source

instance Hex.Conway.instPrimeModulus557 :

ZMod64.PrimeModulus 557

Prime modulus for characteristic 557.

source

instance Hex.Conway.bounds563 :

ZMod64.Bounds 563

Word bounds for characteristic 563.

source

theorem Hex.Conway.prime_563 :

Nat.Prime 563

Primality of characteristic 563.

source

instance Hex.Conway.instPrimeModulus563 :

ZMod64.PrimeModulus 563

Prime modulus for characteristic 563.

source

instance Hex.Conway.bounds569 :

ZMod64.Bounds 569

Word bounds for characteristic 569.

source

theorem Hex.Conway.prime_569 :

Nat.Prime 569

Primality of characteristic 569.

source

instance Hex.Conway.instPrimeModulus569 :

ZMod64.PrimeModulus 569

Prime modulus for characteristic 569.

source

instance Hex.Conway.bounds571 :

ZMod64.Bounds 571

Word bounds for characteristic 571.

source

theorem Hex.Conway.prime_571 :

Nat.Prime 571

Primality of characteristic 571.

source

instance Hex.Conway.instPrimeModulus571 :

ZMod64.PrimeModulus 571

Prime modulus for characteristic 571.

source

instance Hex.Conway.bounds577 :

ZMod64.Bounds 577

Word bounds for characteristic 577.

source

theorem Hex.Conway.prime_577 :

Nat.Prime 577

Primality of characteristic 577.

source

instance Hex.Conway.instPrimeModulus577 :

ZMod64.PrimeModulus 577

Prime modulus for characteristic 577.

source

instance Hex.Conway.bounds587 :

ZMod64.Bounds 587

Word bounds for characteristic 587.

source

theorem Hex.Conway.prime_587 :

Nat.Prime 587

Primality of characteristic 587.

source

instance Hex.Conway.instPrimeModulus587 :

ZMod64.PrimeModulus 587

Prime modulus for characteristic 587.

source

instance Hex.Conway.bounds593 :

ZMod64.Bounds 593

Word bounds for characteristic 593.

source

theorem Hex.Conway.prime_593 :

Nat.Prime 593

Primality of characteristic 593.

source

instance Hex.Conway.instPrimeModulus593 :

ZMod64.PrimeModulus 593

Prime modulus for characteristic 593.

source

instance Hex.Conway.bounds599 :

ZMod64.Bounds 599

Word bounds for characteristic 599.

source

theorem Hex.Conway.prime_599 :

Nat.Prime 599

Primality of characteristic 599.

source

instance Hex.Conway.instPrimeModulus599 :

ZMod64.PrimeModulus 599

Prime modulus for characteristic 599.

source

instance Hex.Conway.bounds601 :

ZMod64.Bounds 601

Word bounds for characteristic 601.

source

theorem Hex.Conway.prime_601 :

Nat.Prime 601

Primality of characteristic 601.

source

instance Hex.Conway.instPrimeModulus601 :

ZMod64.PrimeModulus 601

Prime modulus for characteristic 601.

source

instance Hex.Conway.bounds607 :

ZMod64.Bounds 607

Word bounds for characteristic 607.

source

theorem Hex.Conway.prime_607 :

Nat.Prime 607

Primality of characteristic 607.

source

instance Hex.Conway.instPrimeModulus607 :

ZMod64.PrimeModulus 607

Prime modulus for characteristic 607.

source

instance Hex.Conway.bounds613 :

ZMod64.Bounds 613

Word bounds for characteristic 613.

source

theorem Hex.Conway.prime_613 :

Nat.Prime 613

Primality of characteristic 613.

source

instance Hex.Conway.instPrimeModulus613 :

ZMod64.PrimeModulus 613

Prime modulus for characteristic 613.

source

instance Hex.Conway.bounds617 :

ZMod64.Bounds 617

Word bounds for characteristic 617.

source

theorem Hex.Conway.prime_617 :

Nat.Prime 617

Primality of characteristic 617.

source

instance Hex.Conway.instPrimeModulus617 :

ZMod64.PrimeModulus 617

Prime modulus for characteristic 617.

source

instance Hex.Conway.bounds619 :

ZMod64.Bounds 619

Word bounds for characteristic 619.

source

theorem Hex.Conway.prime_619 :

Nat.Prime 619

Primality of characteristic 619.

source

instance Hex.Conway.instPrimeModulus619 :

ZMod64.PrimeModulus 619

Prime modulus for characteristic 619.

source

instance Hex.Conway.bounds631 :

ZMod64.Bounds 631

Word bounds for characteristic 631.

source

theorem Hex.Conway.prime_631 :

Nat.Prime 631

Primality of characteristic 631.

source

instance Hex.Conway.instPrimeModulus631 :

ZMod64.PrimeModulus 631

Prime modulus for characteristic 631.

source

instance Hex.Conway.bounds641 :

ZMod64.Bounds 641

Word bounds for characteristic 641.

source

theorem Hex.Conway.prime_641 :

Nat.Prime 641

Primality of characteristic 641.

source

instance Hex.Conway.instPrimeModulus641 :

ZMod64.PrimeModulus 641

Prime modulus for characteristic 641.

source

instance Hex.Conway.bounds643 :

ZMod64.Bounds 643

Word bounds for characteristic 643.

source

theorem Hex.Conway.prime_643 :

Nat.Prime 643

Primality of characteristic 643.

source

instance Hex.Conway.instPrimeModulus643 :

ZMod64.PrimeModulus 643

Prime modulus for characteristic 643.

source

instance Hex.Conway.bounds647 :

ZMod64.Bounds 647

Word bounds for characteristic 647.

source

theorem Hex.Conway.prime_647 :

Nat.Prime 647

Primality of characteristic 647.

source

instance Hex.Conway.instPrimeModulus647 :

ZMod64.PrimeModulus 647

Prime modulus for characteristic 647.

source

instance Hex.Conway.bounds653 :

ZMod64.Bounds 653

Word bounds for characteristic 653.

source

theorem Hex.Conway.prime_653 :

Nat.Prime 653

Primality of characteristic 653.

source

instance Hex.Conway.instPrimeModulus653 :

ZMod64.PrimeModulus 653

Prime modulus for characteristic 653.

source

instance Hex.Conway.bounds659 :

ZMod64.Bounds 659

Word bounds for characteristic 659.

source

theorem Hex.Conway.prime_659 :

Nat.Prime 659

Primality of characteristic 659.

source

instance Hex.Conway.instPrimeModulus659 :

ZMod64.PrimeModulus 659

Prime modulus for characteristic 659.

source

instance Hex.Conway.bounds661 :

ZMod64.Bounds 661

Word bounds for characteristic 661.

source

theorem Hex.Conway.prime_661 :

Nat.Prime 661

Primality of characteristic 661.

source

instance Hex.Conway.instPrimeModulus661 :

ZMod64.PrimeModulus 661

Prime modulus for characteristic 661.

source

instance Hex.Conway.bounds673 :

ZMod64.Bounds 673

Word bounds for characteristic 673.

source

theorem Hex.Conway.prime_673 :

Nat.Prime 673

Primality of characteristic 673.

source

instance Hex.Conway.instPrimeModulus673 :

ZMod64.PrimeModulus 673

Prime modulus for characteristic 673.

source

instance Hex.Conway.bounds677 :

ZMod64.Bounds 677

Word bounds for characteristic 677.

source

theorem Hex.Conway.prime_677 :

Nat.Prime 677

Primality of characteristic 677.

source

instance Hex.Conway.instPrimeModulus677 :

ZMod64.PrimeModulus 677

Prime modulus for characteristic 677.

source

instance Hex.Conway.bounds683 :

ZMod64.Bounds 683

Word bounds for characteristic 683.

source

theorem Hex.Conway.prime_683 :

Nat.Prime 683

Primality of characteristic 683.

source

instance Hex.Conway.instPrimeModulus683 :

ZMod64.PrimeModulus 683

Prime modulus for characteristic 683.

source

instance Hex.Conway.bounds691 :

ZMod64.Bounds 691

Word bounds for characteristic 691.

source

theorem Hex.Conway.prime_691 :

Nat.Prime 691

Primality of characteristic 691.

source

instance Hex.Conway.instPrimeModulus691 :

ZMod64.PrimeModulus 691

Prime modulus for characteristic 691.

source

instance Hex.Conway.bounds701 :

ZMod64.Bounds 701

Word bounds for characteristic 701.

source

theorem Hex.Conway.prime_701 :

Nat.Prime 701

Primality of characteristic 701.

source

instance Hex.Conway.instPrimeModulus701 :

ZMod64.PrimeModulus 701

Prime modulus for characteristic 701.

source

instance Hex.Conway.bounds709 :

ZMod64.Bounds 709

Word bounds for characteristic 709.

source

theorem Hex.Conway.prime_709 :

Nat.Prime 709

Primality of characteristic 709.

source

instance Hex.Conway.instPrimeModulus709 :

ZMod64.PrimeModulus 709

Prime modulus for characteristic 709.

source

instance Hex.Conway.bounds719 :

ZMod64.Bounds 719

Word bounds for characteristic 719.

source

theorem Hex.Conway.prime_719 :

Nat.Prime 719

Primality of characteristic 719.

source

instance Hex.Conway.instPrimeModulus719 :

ZMod64.PrimeModulus 719

Prime modulus for characteristic 719.

source

instance Hex.Conway.bounds727 :

ZMod64.Bounds 727

Word bounds for characteristic 727.

source

theorem Hex.Conway.prime_727 :

Nat.Prime 727

Primality of characteristic 727.

source

instance Hex.Conway.instPrimeModulus727 :

ZMod64.PrimeModulus 727

Prime modulus for characteristic 727.

source

instance Hex.Conway.bounds733 :

ZMod64.Bounds 733

Word bounds for characteristic 733.

source

theorem Hex.Conway.prime_733 :

Nat.Prime 733

Primality of characteristic 733.

source

instance Hex.Conway.instPrimeModulus733 :

ZMod64.PrimeModulus 733

Prime modulus for characteristic 733.

source

instance Hex.Conway.bounds739 :

ZMod64.Bounds 739

Word bounds for characteristic 739.

source

theorem Hex.Conway.prime_739 :

Nat.Prime 739

Primality of characteristic 739.

source

instance Hex.Conway.instPrimeModulus739 :

ZMod64.PrimeModulus 739

Prime modulus for characteristic 739.

source

instance Hex.Conway.bounds743 :

ZMod64.Bounds 743

Word bounds for characteristic 743.

source

theorem Hex.Conway.prime_743 :

Nat.Prime 743

Primality of characteristic 743.

source

instance Hex.Conway.instPrimeModulus743 :

ZMod64.PrimeModulus 743

Prime modulus for characteristic 743.

source

instance Hex.Conway.bounds751 :

ZMod64.Bounds 751

Word bounds for characteristic 751.

source

theorem Hex.Conway.prime_751 :

Nat.Prime 751

Primality of characteristic 751.

source

instance Hex.Conway.instPrimeModulus751 :

ZMod64.PrimeModulus 751

Prime modulus for characteristic 751.

source

instance Hex.Conway.bounds757 :

ZMod64.Bounds 757

Word bounds for characteristic 757.

source

theorem Hex.Conway.prime_757 :

Nat.Prime 757

Primality of characteristic 757.

source

instance Hex.Conway.instPrimeModulus757 :

ZMod64.PrimeModulus 757

Prime modulus for characteristic 757.

source

instance Hex.Conway.bounds761 :

ZMod64.Bounds 761

Word bounds for characteristic 761.

source

theorem Hex.Conway.prime_761 :

Nat.Prime 761

Primality of characteristic 761.

source

instance Hex.Conway.instPrimeModulus761 :

ZMod64.PrimeModulus 761

Prime modulus for characteristic 761.

source

instance Hex.Conway.bounds769 :

ZMod64.Bounds 769

Word bounds for characteristic 769.

source

theorem Hex.Conway.prime_769 :

Nat.Prime 769

Primality of characteristic 769.

source

instance Hex.Conway.instPrimeModulus769 :

ZMod64.PrimeModulus 769

Prime modulus for characteristic 769.

source

instance Hex.Conway.bounds773 :

ZMod64.Bounds 773

Word bounds for characteristic 773.

source

theorem Hex.Conway.prime_773 :

Nat.Prime 773

Primality of characteristic 773.

source

instance Hex.Conway.instPrimeModulus773 :

ZMod64.PrimeModulus 773

Prime modulus for characteristic 773.

source

instance Hex.Conway.bounds787 :

ZMod64.Bounds 787

Word bounds for characteristic 787.

source

theorem Hex.Conway.prime_787 :

Nat.Prime 787

Primality of characteristic 787.

source

instance Hex.Conway.instPrimeModulus787 :

ZMod64.PrimeModulus 787

Prime modulus for characteristic 787.

source

instance Hex.Conway.bounds797 :

ZMod64.Bounds 797

Word bounds for characteristic 797.

source

theorem Hex.Conway.prime_797 :

Nat.Prime 797

Primality of characteristic 797.

source

instance Hex.Conway.instPrimeModulus797 :

ZMod64.PrimeModulus 797

Prime modulus for characteristic 797.

source

instance Hex.Conway.bounds809 :

ZMod64.Bounds 809

Word bounds for characteristic 809.

source

theorem Hex.Conway.prime_809 :

Nat.Prime 809

Primality of characteristic 809.

source

instance Hex.Conway.instPrimeModulus809 :

ZMod64.PrimeModulus 809

Prime modulus for characteristic 809.

source

instance Hex.Conway.bounds811 :

ZMod64.Bounds 811

Word bounds for characteristic 811.

source

theorem Hex.Conway.prime_811 :

Nat.Prime 811

Primality of characteristic 811.

source

instance Hex.Conway.instPrimeModulus811 :

ZMod64.PrimeModulus 811

Prime modulus for characteristic 811.

source

instance Hex.Conway.bounds821 :

ZMod64.Bounds 821

Word bounds for characteristic 821.

source

theorem Hex.Conway.prime_821 :

Nat.Prime 821

Primality of characteristic 821.

source

instance Hex.Conway.instPrimeModulus821 :

ZMod64.PrimeModulus 821

Prime modulus for characteristic 821.

source

instance Hex.Conway.bounds823 :

ZMod64.Bounds 823

Word bounds for characteristic 823.

source

theorem Hex.Conway.prime_823 :

Nat.Prime 823

Primality of characteristic 823.

source

instance Hex.Conway.instPrimeModulus823 :

ZMod64.PrimeModulus 823

Prime modulus for characteristic 823.

source

instance Hex.Conway.bounds827 :

ZMod64.Bounds 827

Word bounds for characteristic 827.

source

theorem Hex.Conway.prime_827 :

Nat.Prime 827

Primality of characteristic 827.

source

instance Hex.Conway.instPrimeModulus827 :

ZMod64.PrimeModulus 827

Prime modulus for characteristic 827.

source

instance Hex.Conway.bounds829 :

ZMod64.Bounds 829

Word bounds for characteristic 829.

source

theorem Hex.Conway.prime_829 :

Nat.Prime 829

Primality of characteristic 829.

source

instance Hex.Conway.instPrimeModulus829 :

ZMod64.PrimeModulus 829

Prime modulus for characteristic 829.

source

instance Hex.Conway.bounds839 :

ZMod64.Bounds 839

Word bounds for characteristic 839.

source

theorem Hex.Conway.prime_839 :

Nat.Prime 839

Primality of characteristic 839.

source

instance Hex.Conway.instPrimeModulus839 :

ZMod64.PrimeModulus 839

Prime modulus for characteristic 839.

source

instance Hex.Conway.bounds853 :

ZMod64.Bounds 853

Word bounds for characteristic 853.

source

theorem Hex.Conway.prime_853 :

Nat.Prime 853

Primality of characteristic 853.

source

instance Hex.Conway.instPrimeModulus853 :

ZMod64.PrimeModulus 853

Prime modulus for characteristic 853.

source

instance Hex.Conway.bounds857 :

ZMod64.Bounds 857

Word bounds for characteristic 857.

source

theorem Hex.Conway.prime_857 :

Nat.Prime 857

Primality of characteristic 857.

source

instance Hex.Conway.instPrimeModulus857 :

ZMod64.PrimeModulus 857

Prime modulus for characteristic 857.

source

instance Hex.Conway.bounds859 :

ZMod64.Bounds 859

Word bounds for characteristic 859.

source

theorem Hex.Conway.prime_859 :

Nat.Prime 859

Primality of characteristic 859.

source

instance Hex.Conway.instPrimeModulus859 :

ZMod64.PrimeModulus 859

Prime modulus for characteristic 859.

source

instance Hex.Conway.bounds863 :

ZMod64.Bounds 863

Word bounds for characteristic 863.

source

theorem Hex.Conway.prime_863 :

Nat.Prime 863

Primality of characteristic 863.

source

instance Hex.Conway.instPrimeModulus863 :

ZMod64.PrimeModulus 863

Prime modulus for characteristic 863.

source

instance Hex.Conway.bounds877 :

ZMod64.Bounds 877

Word bounds for characteristic 877.

source

theorem Hex.Conway.prime_877 :

Nat.Prime 877

Primality of characteristic 877.

source

instance Hex.Conway.instPrimeModulus877 :

ZMod64.PrimeModulus 877

Prime modulus for characteristic 877.

source

instance Hex.Conway.bounds881 :

ZMod64.Bounds 881

Word bounds for characteristic 881.

source

theorem Hex.Conway.prime_881 :

Nat.Prime 881

Primality of characteristic 881.

source

instance Hex.Conway.instPrimeModulus881 :

ZMod64.PrimeModulus 881

Prime modulus for characteristic 881.

source

instance Hex.Conway.bounds883 :

ZMod64.Bounds 883

Word bounds for characteristic 883.

source

theorem Hex.Conway.prime_883 :

Nat.Prime 883

Primality of characteristic 883.

source

instance Hex.Conway.instPrimeModulus883 :

ZMod64.PrimeModulus 883

Prime modulus for characteristic 883.

source

instance Hex.Conway.bounds887 :

ZMod64.Bounds 887

Word bounds for characteristic 887.

source

theorem Hex.Conway.prime_887 :

Nat.Prime 887

Primality of characteristic 887.

source

instance Hex.Conway.instPrimeModulus887 :

ZMod64.PrimeModulus 887

Prime modulus for characteristic 887.

source

instance Hex.Conway.bounds907 :

ZMod64.Bounds 907

Word bounds for characteristic 907.

source

theorem Hex.Conway.prime_907 :

Nat.Prime 907

Primality of characteristic 907.

source

instance Hex.Conway.instPrimeModulus907 :

ZMod64.PrimeModulus 907

Prime modulus for characteristic 907.

source

instance Hex.Conway.bounds911 :

ZMod64.Bounds 911

Word bounds for characteristic 911.

source

theorem Hex.Conway.prime_911 :

Nat.Prime 911

Primality of characteristic 911.

source

instance Hex.Conway.instPrimeModulus911 :

ZMod64.PrimeModulus 911

Prime modulus for characteristic 911.

source

instance Hex.Conway.bounds919 :

ZMod64.Bounds 919

Word bounds for characteristic 919.

source

theorem Hex.Conway.prime_919 :

Nat.Prime 919

Primality of characteristic 919.

source

instance Hex.Conway.instPrimeModulus919 :

ZMod64.PrimeModulus 919

Prime modulus for characteristic 919.

source

instance Hex.Conway.bounds929 :

ZMod64.Bounds 929

Word bounds for characteristic 929.

source

theorem Hex.Conway.prime_929 :

Nat.Prime 929

Primality of characteristic 929.

source

instance Hex.Conway.instPrimeModulus929 :

ZMod64.PrimeModulus 929

Prime modulus for characteristic 929.

source

instance Hex.Conway.bounds937 :

ZMod64.Bounds 937

Word bounds for characteristic 937.

source

theorem Hex.Conway.prime_937 :

Nat.Prime 937

Primality of characteristic 937.

source

instance Hex.Conway.instPrimeModulus937 :

ZMod64.PrimeModulus 937

Prime modulus for characteristic 937.

source

instance Hex.Conway.bounds941 :

ZMod64.Bounds 941

Word bounds for characteristic 941.

source

theorem Hex.Conway.prime_941 :

Nat.Prime 941

Primality of characteristic 941.

source

instance Hex.Conway.instPrimeModulus941 :

ZMod64.PrimeModulus 941

Prime modulus for characteristic 941.

source

instance Hex.Conway.bounds947 :

ZMod64.Bounds 947

Word bounds for characteristic 947.

source

theorem Hex.Conway.prime_947 :

Nat.Prime 947

Primality of characteristic 947.

source

instance Hex.Conway.instPrimeModulus947 :

ZMod64.PrimeModulus 947

Prime modulus for characteristic 947.

source

instance Hex.Conway.bounds953 :

ZMod64.Bounds 953

Word bounds for characteristic 953.

source

theorem Hex.Conway.prime_953 :

Nat.Prime 953

Primality of characteristic 953.

source

instance Hex.Conway.instPrimeModulus953 :

ZMod64.PrimeModulus 953

Prime modulus for characteristic 953.

source

instance Hex.Conway.bounds967 :

ZMod64.Bounds 967

Word bounds for characteristic 967.

source

theorem Hex.Conway.prime_967 :

Nat.Prime 967

Primality of characteristic 967.

source

instance Hex.Conway.instPrimeModulus967 :

ZMod64.PrimeModulus 967

Prime modulus for characteristic 967.

source

instance Hex.Conway.bounds971 :

ZMod64.Bounds 971

Word bounds for characteristic 971.

source

theorem Hex.Conway.prime_971 :

Nat.Prime 971

Primality of characteristic 971.

source

instance Hex.Conway.instPrimeModulus971 :

ZMod64.PrimeModulus 971

Prime modulus for characteristic 971.

source

instance Hex.Conway.bounds977 :

ZMod64.Bounds 977

Word bounds for characteristic 977.

source

theorem Hex.Conway.prime_977 :

Nat.Prime 977

Primality of characteristic 977.

source

instance Hex.Conway.instPrimeModulus977 :

ZMod64.PrimeModulus 977

Prime modulus for characteristic 977.

source

instance Hex.Conway.bounds983 :

ZMod64.Bounds 983

Word bounds for characteristic 983.

source

theorem Hex.Conway.prime_983 :

Nat.Prime 983

Primality of characteristic 983.

source

instance Hex.Conway.instPrimeModulus983 :

ZMod64.PrimeModulus 983

Prime modulus for characteristic 983.

source

instance Hex.Conway.bounds991 :

ZMod64.Bounds 991

Word bounds for characteristic 991.

source

theorem Hex.Conway.prime_991 :

Nat.Prime 991

Primality of characteristic 991.

source

instance Hex.Conway.instPrimeModulus991 :

ZMod64.PrimeModulus 991

Prime modulus for characteristic 991.

source

instance Hex.Conway.bounds997 :

ZMod64.Bounds 997

Word bounds for characteristic 997.

source

theorem Hex.Conway.prime_997 :

Nat.Prime 997

Primality of characteristic 997.

source

instance Hex.Conway.instPrimeModulus997 :

ZMod64.PrimeModulus 997

Prime modulus for characteristic 997.