Commit 2024-12-10 17:35 57bf4011

View on Github →

feat: lower bound on the Ruzsa-Szemerédi problem (#19000) From LeanCamCombi

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean

added theorem SimpleGraph.LocallyLinear.le_ruzsaSzemerediNumber

added theorem addRothNumber_le_ruzsaSzemerediNumber

added theorem rothNumberNat_le_ruzsaSzemerediNumberNat'

added theorem rothNumberNat_le_ruzsaSzemerediNumberNat

added theorem ruzsaSzemerediNumberNat_asymptotic_lower_bound

added theorem ruzsaSzemerediNumberNat_card

added theorem ruzsaSzemerediNumberNat_le

added theorem ruzsaSzemerediNumberNat_lower_bound

added theorem ruzsaSzemerediNumberNat_mono

added theorem ruzsaSzemerediNumberNat_one

added theorem ruzsaSzemerediNumberNat_two

added theorem ruzsaSzemerediNumberNat_zero

added theorem ruzsaSzemerediNumber_congr

added theorem ruzsaSzemerediNumber_le

added theorem ruzsaSzemerediNumber_mono

added theorem ruzsaSzemerediNumber_spec