OAI/Combinatorics/ProgressionColoring/DigitProductBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.QuantitativeVanDerWaerden.cyclic_binary_product_lower line 9

   Source documentation

   The product of any number of copies of one cyclic Boolean coloring.

   theorem cyclic_binary_product_lower {N k m : ℕ} {C : ZMod N → Bool}
       (hN : 2 ≤ N) (hk : 2 ≤ k) (hC : CyclicAvoids C k) :
       N ^ m < W (2 ^ m) k := by
   …

   Mentions: OAI.QuantitativeVanDerWaerden.CyclicAvoids

2. theorem OAI.QuantitativeVanDerWaerden.cyclic_binary_color_lower line 15