Theorems · Theorem · combinatorics

Combinatorics.exists_mono_homothetic_copy

• 1000+ list: Van der Waerden's theorem

∀ {M : Type u_5} {κ : Type u_6} [inst : AddCommMonoid M] (S : Finset M) [Finite κ] (C : M → κ),
  ∃ a > 0, ∃ b c, ∀ s ∈ S, C (a • s + b) = c

A generalization of Van der Waerden's theorem: if M is a finitely colored commutative monoid, and S is a finite subset, then there exists a monochromatic homothetic copy of S.

Defined in

Mathlib.Combinatorics.HalesJewett

Cited by

0 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidFinite