Commit 2023-03-01 02:42 7a0dd7b2

feat(combinatorics/simple_graph/regularity/bound): Local positivity extension (#18368) I was finding myself writing long positivity proofs that relied only on a few Szemerédi Regularity Lemma-specific lemmas before applying a bunch of usual positivity lemmas. This provides a SRL-specific positivity extension, which I turn on locally in the files internal to the proof of SRL. It works great and has significantly reduced the clutter.