Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - chore(fintype/card_embedding): generalize instances #12775

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - chore(fintype/card_embedding): generalize instances #12775

wants to merge 10 commits into from

Conversation

ericrbg
Copy link
Collaborator

@ericrbg ericrbg commented Mar 17, 2022

Open in Gitpod

@ericrbg ericrbg added the awaiting-review The author would like community review of the PR label Mar 17, 2022
@ericrbg @urkud
Update src/data/fintype/card_embedding.lean
d209e29 
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@urkud
Golf
9d04837
@urkud
Merge branch 'ericrbg/generalize_card_embedding' of ssh://github.com/…
d37d508 
…leanprover-community/mathlib into ericrbg/generalize_card_embedding
urkud and others added 3 commits March 19, 2022 11:03
@urkud
Fix
71f89e4
@urkud
Fix
a429653
@urkud @eric-wieser
Update src/logic/embedding.lean
aa9cc19 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@jcommelin
Copy link
Member

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Mar 24, 2022
bors bot pushed a commit that referenced this pull request Mar 24, 2022
@ericrbg @urkud
chore(fintype/card_embedding): generalize instances (#12775)
0faebd2 
Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@bors
Copy link

bors bot commented Mar 24, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(fintype/card_embedding): generalize instances [Merged by Bors] - chore(fintype/card_embedding): generalize instances Mar 24, 2022
@bors bors bot closed this Mar 24, 2022
@bors bors bot deleted the ericrbg/generalize_card_embedding branch March 24, 2022 12:01
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@urkud urkud urkud left review comments

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

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@ericrbg @jcommelin @urkud @eric-wieser