mathlib3

8f774b71 - feat(combinatorics/simple_graph/regularity/bound): `positivity` extension (#16639)

feat(combinatorics/simple_graph/regularity/bound): `positivity` extension (#16639) Add a `positivity` extension for `szemeredi_regularity.initial_bound` and `szemeredi_regularity.bound`.