Nailin Guan
Nailin Guan
Sorry, where is the "nitpick comment"? I didn't found it. Do you mean to use obtain rather than rcases?
The import problem is fixed for now in this PR, but I still have a problem here : I have two theorems using the import not currently in `OpenSubgroup.lean`, it...
Theorem needing more import moved to new file.
Additive version of the theory of open subgroup in clopen neighborhood is added. I think most lemmas about this would only be used only here (I think we can always...
This PR is deprecated, the same final result woud be moved to #18377 instead with better proof.
This PR is originally from #24921
This PR is originally from #25230
This PR is originally from #24922
I handed this PR out to another collaborator, the new PR is #33220.