mathlib

7a0dd7b2 - feat(combinatorics/simple_graph/regularity/bound): Local `positivity` extension (#18368)

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.