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
feat(archive): add proof of sensitivity conjecture #1553
Conversation
Co-Authored-By: Johan Commelin <johan@commelin.net>
this leads to loops with `subtype.fintype` under the right decidable_eq assumptions
-- a natural number). | ||
variable {n} | ||
|
||
lemma succ_n_eq (p q : Q (n+1)) : p = q ↔ (p 0 = q 0 ∧ π p = π q) := |
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.
I don't really understand this name... but eq_iff_fst_eq_and_proj_eq
is very verbose.
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, it's not really important, but I'm not sure what to call it. Your suggestion is very long.
Looks good. Shall we merge? |
Patrick did a nice job of making this presentable over the summer, so I suspect there's not much more work to be done. |
…ity#1553) * feat(*): various lemmas from the sensitivity project * fix proof broken by nonterminal simp * Update src/linear_algebra/dual.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * lint dual.lean * remove decidable_mem_of_fintype instance this leads to loops with `subtype.fintype` under the right decidable_eq assumptions * dual_lc is invalid simp lemma * fix namespace * add extra lemma * feat(archive): add proof of sensitivity conjecture * suggestions from Johan * undo removed whitespace * update header
Moving the formalization from https://github.com/leanprover-community/lean-sensitivity to the mathlib archive.
This builds on #1550 which locates the lemmas from
for_mathlib.lean
throughout the library. When that's merged, I'll rebase the last commit here.This is coauthored with @rwbarton @jcommelin @jesse-michael-han @ChrisHughes24 @PatrickMassot
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list