-
Notifications
You must be signed in to change notification settings - Fork 298
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] - refactor(group_theory/perm/*): disjoint and support in own file #7450
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Splitting this is definitely a good idea, and the few renames are also good. It'll conflict with every other permutation PR though, so it may take some care on the part of the maintainers.
I can keep updating this PR if those get merged first, or we can try to
merge this quickly.
…On Mon, May 3, 2021 at 6:56 PM Aaron Anderson ***@***.***> wrote:
***@***.**** approved this pull request.
Splitting this is definitely a good idea, and the few renames are also
good. It'll conflict with every other permutation PR though, so it may take
some care on the part of the maintainers.
—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
<#7450 (review)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ABIYHBRNE7X4LCHINBUJAZDTL4SZPANCNFSM44BTTR7Q>
.
|
I took that description basically from the disjoint docstring below. I've
pushed a commit clarifying it.
…On Mon, May 3, 2021 at 7:10 PM tb65536 ***@***.***> wrote:
***@***.**** approved this pull request.
------------------------------
In src/group_theory/perm/support.lean
<#7450 (comment)>
:
> +* `equiv.perm.disjoint`: two permutations `f` and `g` are `disjoint` iff their `support`
+ are disjoint.
This sounds like a description of disjoint_iff_disjoint_support, rather
than a definition of disjoint.
—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
<#7450 (review)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ABIYHBUAOQPBCINPHE2CEUDTL4UODANCNFSM44BTTR7Q>
.
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Let's get this merged quickly before it causes conflicts.
bors r+
The group_theory/perm/sign file was getting large and too broad in scope. This refactor pulls out `perm.support`, `perm.is_swap`, and `perm.disjoint` into a separate file. A simpler version of #7118.
Pull request successfully merged into master. Build succeeded: |
The group_theory/perm/sign file was getting large and too broad in scope. This refactor pulls out
perm.support
,perm.is_swap
, andperm.disjoint
into a separate file.A simpler version of #7118.