mathlib

8ff9c0e6 - feat(group_theory/order_of_element): add is_cyclic_of_prime_card (#5172)

feat(group_theory/order_of_element): add is_cyclic_of_prime_card (#5172) Add `is_cyclic_of_prime_card`, which says if a group has prime order, then it is cyclic. I also added `eq_top_of_card_eq` which says a subgroup is `top` when it has the same size as the group, not sure where that should be in the file.