Commit 2024-07-18 10:47 3050e820
View on Github →feat(Algebra/Group/SemiconjBy): relating SemiconjBy to orderOf (#14674)
this PR adds SemiconjBy.orderOf_eq, proving that semiconjugates have the same order.
it also adds SemiconjBy.eq_one_iff, which is used to prove the previous statement.
relevant zulip thread:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/group.20problem