mathlib

179dcdea - refactor(group_theory/order_of_element): Remove `fintype` hypothesis from `pow_coprime` (#16989)

refactor(group_theory/order_of_element): Remove `fintype` hypothesis from `pow_coprime` (#16989) This PR removes the `[fintype G]` hypothesis from `pow_coprime (h : coprime (card G) n) : G ≃ G` (the bijection given by the `n`th power map).