Theorems · Definition · combinatorics
ruzsaSzemerediNumber
(α : Type u_1) → [DecidableEq α] → [Fintype α] → ℕ
The Ruzsa-Szemerédi number of a fintype is the maximum number of edges a locally linear
graph on that type can have.
In other words, ruzsaSzemerediNumber α is the maximum number of edges a graph on α can have such
that each edge belongs to exactly one triangle.
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEqFintype
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypestatement and proof · cited by 7,736
- SimpleGraphproof · cited by 3,072
- Finset.cardproof · cited by 2,327
- Fintype.cardproof · cited by 1,386
- SimpleGraph.Adjproof · cited by 1,346
- Nat.chooseproof · cited by 494
- SimpleGraph.cliqueFinsetproof · cited by 26
- Nat.findGreatestproof · cited by 25
- SimpleGraph.LocallyLinearproof · cited by 9
Cited by9
Results whose statement or proof uses this declaration.
- ruzsaSzemerediNumberNatproof · cited by 10
- ruzsaSzemerediNumber_monostatement · cited by 2
- ruzsaSzemerediNumber_congrstatement · cited by 1
- ruzsaSzemerediNumber_lestatement · cited by 1
- SimpleGraph.LocallyLinear.le_ruzsaSzemerediNumberstatement · cited by 1
- addRothNumber_le_ruzsaSzemerediNumberstatement and proof · cited by 1
- ruzsaSzemerediNumberNat_cardstatement · cited by 0
- ruzsaSzemerediNumber_specstatement · cited by 0
- ruzsaSzemerediNumber.congr_simpstatement and proof · cited by 0