-
Notifications
You must be signed in to change notification settings - Fork 235
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: results about List.orderedInsert
#11191
Conversation
Mathlib/Data/List/Sort.lean
Outdated
simp [refl x] at h | ||
|
||
/-- Inserting then erasing an element that is absent is the identity. -/ | ||
theorem erase_orderedInsert_of_nmem [DecidableEq α] |
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 use nmem
as a naming convention anywhere?
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.
yes, but 10x less than not_mem
, and not in the List
namespace; edited.
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Thanks! maintainer merge |
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
Thanks! bors merge |
I suspect I will need some of these for #10660
Pull request successfully merged into master. Build succeeded: |
List.orderedInsert
List.orderedInsert
I suspect I will need some of these for #10660
I suspect I will need some of these for #10660
I suspect I will need some of these for #10660
I suspect I will need some of these for #10660
I suspect I will need some of these for #10660
I suspect I will need some of these for #10660