Theorem ruzsaSzemerediNumberNat_mono

Modification history

2025-10-27 16:35
Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
feat(gcongr): support `@[gcongr]` for `Monotone` and friends (#28339) …
Modified ruzsaSzemerediNumberNat_monoView on Github →
2025-10-17 14:39
Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
chore: use `grw`, `gcongr` more (#30508) …
Modified ruzsaSzemerediNumberNat_monoView on Github →
2024-12-10 17:35
Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
feat: lower bound on the Ruzsa-Szemerédi problem (#19000) …
Added ruzsaSzemerediNumberNat_monoView on Github →