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

feat(algebra/char_zero): cast_injective for integers #14458

Closed
wants to merge 8 commits into from
Closed

feat(algebra/char_zero): cast_injective for integers #14458

wants to merge 8 commits into from

Conversation

joneugster
Copy link
Collaborator

@joneugster joneugster commented May 30, 2022 •
edited
Loading

cast_injective extended to integers.

My proof feels very manual and I think there should be a much quicker way...

Open in Gitpod

@joneugster joneugster added help-wanted The author needs attention to resolve issues medium awaiting-review The author would like community review of the PR blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels May 30, 2022
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label May 30, 2022
@joneugster joneugster added the WIP Work in progress label May 30, 2022
@joneugster joneugster removed medium awaiting-review The author would like community review of the PR labels May 30, 2022
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label May 30, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@joneugster joneugster closed this May 30, 2022
@joneugster joneugster removed the help-wanted The author needs attention to resolve issues label May 30, 2022
@joneugster joneugster deleted the char_zero_cast_inj branch June 2, 2022 08:19
@joneugster joneugster added duplicate and removed WIP Work in progress blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Jun 2, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

Assignees
No one assigned
Labels
duplicate
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@joneugster @mathlib-dependent-issues-bot @eric-wieser