Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - chore(data/int/basic): remove redundant lemmas #321

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - chore(data/int/basic): remove redundant lemmas #321

wants to merge 3 commits into from

Conversation

semorrison
Copy link
Contributor

No description provided.

@semorrison
Copy link
Contributor Author

semorrison commented Jun 12, 2020 •
edited

Another thing I'm tempted to do is rename all injectivity lemmas currently named *_inj to *.inj, to match the automatically generated ones.

Pros:

  • Be able to identify injectivity lemmas easily (e.g. have library_search ignore them!)

Cons:

  • Not be able to distinguish just from the name between automatically generated injectivity lemmas and hand-written ones.

@gebner
Copy link
Member

gebner commented Jun 17, 2020

bors merge

bors bot pushed a commit that referenced this pull request Jun 17, 2020
@semorrison
chore(data/int/basic): remove redundant lemmas (#321)
4782e3d 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Jun 17, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(data/int/basic): remove redundant lemmas [Merged by Bors] - chore(data/int/basic): remove redundant lemmas Jun 17, 2020
@bors bors bot closed this Jun 17, 2020
@bors bors bot deleted the of_nat_inj branch June 17, 2020 07:47
@semorrison semorrison mentioned this pull request Jun 18, 2020
Closed
bors bot pushed a commit to leanprover-community/mathlib that referenced this pull request Jun 18, 2020
@semorrison
chore(*): update to lean 3.16.3 (#3107)
53af714 
The changes to mathlib are from leanprover-community/lean#321 which removed some redundant lemmas:
* `int.of_nat_inj` -> `int.of_nat.inj`
* `int.neg_succ_of_nat_inj` -> `int.neg_succ_of_nat.inj`
* `nat.succ_inj` -> `nat.succ.inj`



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
cipher1024 pushed a commit to cipher1024/mathlib that referenced this pull request Mar 15, 2022
@semorrison @cipher1024
chore(*): update to lean 3.16.3 (leanprover-community#3107)
bee2517 
The changes to mathlib are from leanprover-community/lean#321 which removed some redundant lemmas:
* `int.of_nat_inj` -> `int.of_nat.inj`
* `int.neg_succ_of_nat_inj` -> `int.neg_succ_of_nat.inj`
* `nat.succ_inj` -> `nat.succ.inj`



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@semorrison @gebner