-
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/cycle/basic): Consolidate API #17898
Conversation
Move the `same_cycle` lemmas before the `is_cycle` ones in order to reduce the diff in #17898. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
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.
Nice cleanups, thanks!
bors d+
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
The bors queue is currently empty, so I will just try going ahead. bors merge |
Reorganise and complete the cycle API: * Previously, `is_cycle` was spelling out the definition of `same_cycle`. Now use it explicitly. * Change binder to semi-implicit in the definition of `is_cycle`. * Add lemmas and iff aliases. * Golf existing proofs using those (mostly invisible from the diff because git decided I am moving the `is_cycle` API) * Improve lemma names, mostly for better dot notation. ## New lemmas * `maps_to.extend_domain` * `surj_on.extend_domain` * `bij_on.extend_domain` * `extend_domain_pow` * `extend_domain_zpow` * `same_cycle.rfl` * `eq.same_cycle` * `same_cycle.conj` * `same_cycle_conj` * `same_cycle_pow_right_iff` * `same_cycle_zpow_right_iff` * `same_cycle.pow_left` * `same_cycle.pow_right` * `same_cycle.zpow_left` * `same_cycle.zpow_left` * `same_cycle.of_pow` * `same_cycle.of_zpow` * `same_cycle_subtype_perm` * `same_cycle.subtype_perm` * `same_cycle_extend_domain` * `is_cycle.conj` * `is_cycle.pow_eq_one_iff'` * `is_cycle.pow_eq_one_iff''` ## Renames * `order_of_is_cycle` → `is_cycle.order_of` * `is_cycle.is_cycle_conj` → `is_cycle.conj` * `is_cycle_of_is_cycle_pow` → `is_cycle.of_pow` * `is_cycle_of_is_cycle_zpow` → `is_cycle.of_zpow` * `same_cycle_cycle` → `is_cycle_iff_same_cycle` * `mem_support_pos_pow_iff_of_lt_order_of` → `support_pow_of_pos_of_lt_order_of` and change the statement to talk about unextensionalised finset equality
Pull request successfully merged into master. Build succeeded: |
Reorganise and complete the cycle API:
is_cycle
was spelling out the definition ofsame_cycle
. Now use it explicitly.is_cycle
.is_cycle
API)New lemmas
maps_to.extend_domain
surj_on.extend_domain
bij_on.extend_domain
extend_domain_pow
extend_domain_zpow
same_cycle.rfl
eq.same_cycle
same_cycle.conj
same_cycle_conj
same_cycle_pow_right_iff
same_cycle_zpow_right_iff
same_cycle.pow_left
same_cycle.pow_right
same_cycle.zpow_left
same_cycle.zpow_left
same_cycle.of_pow
same_cycle.of_zpow
same_cycle_subtype_perm
same_cycle.subtype_perm
same_cycle_extend_domain
is_cycle.conj
is_cycle.pow_eq_one_iff'
is_cycle.pow_eq_one_iff''
Renames
order_of_is_cycle
→is_cycle.order_of
is_cycle.is_cycle_conj
→is_cycle.conj
is_cycle_of_is_cycle_pow
→is_cycle.of_pow
is_cycle_of_is_cycle_zpow
→is_cycle.of_zpow
same_cycle_cycle
→is_cycle_iff_same_cycle
mem_support_pos_pow_iff_of_lt_order_of
→support_pow_of_pos_of_lt_order_of
and change the statement to talk about unextensionalised finset equality