OAI/Combinatorics/ProgressionColoring/CyclicBasic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The common nonzero-step cyclic avoidance predicate. Colors are generic so the constructed Boolean coloring and finite-cardinality transfers use the same definition without a color conversion.

  1. def OAI.QuantitativeVanDerWaerden.CyclicAvoids line 13