OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedPrimeInitialization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Executed prime-modulus initialization from its known width

  1. def OAI.LowSpaceSubsetSum.WordSeedMeasured.primeInitialized line 10
  2. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.primeInitialized_bounded line 21