-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(combinatorics/simple_graph/regularity/bound): Local positivity
extension
#18368
Conversation
|
||
lemma coe_m_add_one_pos : 0 < (m : ℝ) + 1 := nat.cast_add_one_pos _ | ||
lemma coe_m_add_one_pos : 0 < (m : ℝ) + 1 := by positivity |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do we still need this lemma at all? Even before it was just a single library result, but now looks like it might get folded into a positivity
application
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, #18371 uses three times explicitly and it helps elaboration quite a lot.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah I see
maintainer merge |
🚀 Pull request has been placed on the maintainer queue by b-mehta. |
Thanks, bors r+ |
… 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.
Build failed (retrying...): |
… 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.
Build failed (retrying...): |
… 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.
Build failed (retrying...): |
… 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.
Pull request successfully merged into master. Build succeeded: |
positivity
extensionpositivity
extension
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.