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(topology/homotopy/homotopy_group): group
and comm_group
instances for π_n
#15681
Conversation
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
+ A function `f` from a `unique` type is equal to the constant function with value `f default`, and the analogous heq version for dependent functions. + Also changes `Π a : α, Sort v` in the file to `α → Sort v`. Inspired by #14724 (comment)
forgot to label it awaiting-review ... now the main file has been ported to mathlib4 apparently |
Thanks 🎉 bors merge |
…ances for `π_n` (#15681) This PR adds: - Group instance for `π_(n+1)` - Commutative group instance for `π_(n+2)` Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: Junyan Xu <junyanxumath@gmail.com> Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
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. If you want to switch to GitHub's built-in merge queue, visit their help page. |
group
and comm_group
instances for π_n
group
and comm_group
instances for π_n
…3874) just changing explicitness of one variable leanprover-community/mathlib#15681 Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
…eanprover-community#3874) just changing explicitness of one variable leanprover-community/mathlib#15681 Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
This PR adds:
π_(n+1)
π_(n+2)
port: leanprover-community/mathlib4#3874