mathlib3
ac825bfa - feat(group_theory/order_of_element): lemmas about orders of powers of group elements (#17433)

Commit

3 years ago

feat(group_theory/order_of_element): lemmas about orders of powers of group elements (#17433) The lemma `subgroup.mk_eq_one_iff` is unrelated but convenient to include for dependent work.

Author

ocfnash

Parents

c946d609

mathlib3 ac825bfa - feat(group_theory/order_of_element): lemmas about orders of powers of group elements (#17433)

mathlib3
ac825bfa - feat(group_theory/order_of_element): lemmas about orders of powers of group elements (#17433)