OAI/NumberTheory/TwoPoint/Bounds/EncodedPrimeSupport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every prime used by a numerical encoding lies in its declared finite pools.

  1. theorem OAI.TwoPointCorrelations.PrimeWordEncoding.divisor_support_subset line 12