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

Replace old definition of cyclic with new cyclic' #2051

Closed
Alizter opened this issue Aug 6, 2024 · 0 comments · Fixed by #2053
Closed

Replace old definition of cyclic with new cyclic' #2051

Alizter opened this issue Aug 6, 2024 · 0 comments · Fixed by #2053
Labels
cleanup

Comments

@Alizter
Copy link
Collaborator

Alizter commented Aug 6, 2024

In #2050, a new definition of cyclic based on Int is introduced. Replacing the old one is a bit non-trivial however due to its extensive use.

It's also not clear if it is easy to show abgroup_Z is the free group on one generator. I had a quick look, but it seems awkward to prove.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
cleanup
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

replace cyclic with cyclic' Alizter/HoTT
1 participant
@Alizter