Documentation

HexConway.FactorProofs.S0_4

source
theorem Hex.Conway.factorPrime_823 :
Nat.Prime 823

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_827 :
Nat.Prime 827

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_839 :
Nat.Prime 839

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_857 :
Nat.Prime 857

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_877 :
Nat.Prime 877

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_883 :
Nat.Prime 883

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_911 :
Nat.Prime 911

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_919 :
Nat.Prime 919

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_941 :
Nat.Prime 941

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_991 :
Nat.Prime 991

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_1061 :
Nat.Prime 1061

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_1063 :
Nat.Prime 1063

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_1087 :
Nat.Prime 1087

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_1093 :
Nat.Prime 1093

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_1201 :
Nat.Prime 1201

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_1277 :
Nat.Prime 1277

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_1321 :
Nat.Prime 1321

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_1327 :
Nat.Prime 1327

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_1423 :
Nat.Prime 1423

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_1471 :
Nat.Prime 1471

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_1613 :
Nat.Prime 1613

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_1693 :
Nat.Prime 1693

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_1699 :
Nat.Prime 1699

Primality of a multiplicative-order factor or a Pocklington child.

source
theorem Hex.Conway.factorPrime_1723 :
Nat.Prime 1723

Primality of a multiplicative-order factor or a Pocklington child.