Theorems · Theorem · number theory

rothNumberNat_add_le

∀ (M N : ℕ), rothNumberNat (M + N) ≤ rothNumberNat M + rothNumberNat N

The Roth number is a subadditive function. Note that by Fekete's lemma this shows that the limit rothNumberNat N / N exists, but Roth's theorem gives the stronger result that this limit is actually 0.

Defined in

Mathlib.Combinatorics.Additive.AP.Three.Defs

Cited by

0 results in Mathlib

Foundations

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