mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard
verified publisher icon leanprover-community

feat(topology/homotopy/homotopy_group): `group` and `comm_group` instances for `π_n`

Open ralvrz opened this issue 3 years ago • 2 comments

This PR adds:

  • Group instance for π_(n+1)
  • Commutative group instance for π_(n+2)
  • [x] depends on: #16879

Open in Gitpod

ralvrz avatar Jul 25 '22 22:07 ralvrz

Hi @alreadydone please feel free to PR what you consider ready. Lately I've been trying to generalize the auxiliary lemmas and definitions, however I failed to do so satisfactorily and got distracted working towards the next goals. Apologies for leaving this PR unattended, I'll be updating it sometime soon

ralvrz avatar Aug 20 '22 22:08 ralvrz

This PR/issue depends on:

  • ~~leanprover-community/mathlib#16879~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Oct 12 '22 03:10 mathlib-dependent-issues-bot

Hi @alreadydone I've been doing some cleaning in this PR, let me know what needs to be done in order to close it. Thanks!

ralvrz avatar Apr 26 '23 13:04 ralvrz

🚀 Pull request has been placed on the maintainer queue by alreadydone.

github-actions[bot] avatar May 10 '23 18:05 github-actions[bot]

@eric-wieser This PR seems forgotten. Do you have any other comments or do you want another maintainer to take a look?

alreadydone avatar May 24 '23 03:05 alreadydone

forgot to label it awaiting-review ... now the main file has been ported to mathlib4 apparently

alreadydone avatar Jun 03 '23 22:06 alreadydone

Thanks :tada:

bors merge

jcommelin avatar Jun 05 '23 05:06 jcommelin

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here. For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

bors[bot] avatar Jun 05 '23 08:06 bors[bot]