Closed dan323 closed 1 year ago
@SKolodynski do you approve? I am working on ring ideals next.
Sorry I did not notice there are new PR's. I will review them in the next couple of days.
@SKolodynski I am not finished with the one about ideals.
This PR has been merged. I did the merge locally, then applied some changes and pushed the result to GH. I am not sure how can I tell GitHub that so that it does not show these conflicts. If you have an idea for a workflow such that I can modify and merge locally and GitHub knows the PR has been merged please let me know. Otherwise I will close this PR.
You pushed master after merging locally? That will not work. Close this PR
Added some sublocales to avoid carrying
group0
around all the time