Commit 2025-09-29 19:11 426708f3
View on Github →feat(GroupTheory): powers_le_zpowers (#29991)
In a later file because of no earlier import.
Allows for a restatement of orderOf_eq_card_of_forall_mem_zpowers as orderOf_eq_card_of_forall_mem_powers
Add a simp tag for an "obvious" lemma at the same time
On the way to characterization of the torsion subgroup as the sup over all subgroups of roots of unity