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: Add instance of Infinite String #1973
[Merged by Bors] - feat: Add instance of Infinite String #1973
Conversation
Mathlib/Data/Fintype/Card.lean
Outdated
Infinite.of_surjective String.length <| by | ||
intro n | ||
exists (String.replicate n 'x') | ||
exact String.length_replicate n 'x' |
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 think the proof is even shorter if you move it down a few lines and use String.data
instead
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've now changed the proof so it uses the injectivity of String.mk
. I suspect that said injectivity could be proven more concisely, do you have any suggestions in that regard?
bors merge |
This proves that the `String` type is infinite.
Pull request successfully merged into master. Build succeeded:
|
This proves that the `String` type is infinite.
This proves that the `String` type is infinite.
This proves that the `String` type is infinite.
This proves that the
String
type is infinite.