Theorems · Theorem · combinatorics

addRothNumber_le_ruzsaSzemerediNumber

∀ (α : Type u_1) [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : CommRing α] [Fact (IsUnit 2)],
  Fintype.card α * addRothNumber Finset.univ ≤ ruzsaSzemerediNumber (α ⊕ α ⊕ α)

Defined in

Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqCommRingFact