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(analysis): completion of normed group homs #8317

Closed
wants to merge 9 commits into from
Closed

feat(analysis): completion of normed group homs #8317

wants to merge 9 commits into from

Conversation

PatrickMassot
Copy link
Member

From LTE

Open in Gitpod

@PatrickMassot PatrickMassot added the WIP Work in progress label Jul 15, 2021
PatrickMassot and others added 4 commits July 18, 2021 18:00
@PatrickMassot PatrickMassot added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Jul 18, 2021
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jul 18, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jul 22, 2021
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 1, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 1, 2021
@PatrickMassot
Copy link
Member Author

I apologize for the slow motion. I spent one week and a half with a slow computer and extremely unreliable internet access. Hopefully I completed the refactor. This PR is now a huge mess so I'll close it and open separate PRs.

This was referenced Aug 1, 2021
Closed
Closed
@PatrickMassot PatrickMassot mentioned this pull request Aug 1, 2021
Closed
2 tasks
@PatrickMassot PatrickMassot deleted the normed_group_hom_completion branch October 19, 2021 16:10
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

@jcommelin jcommelin jcommelin left review comments

@riccardobrasca riccardobrasca riccardobrasca left review comments

Assignees
No one assigned
Labels
awaiting-review The author would like community review of the PR
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@PatrickMassot @eric-wieser @jcommelin @riccardobrasca