mathlib3

6b183624 - feat(data/zmod/quotient): More API for `orbit_zpowers_equiv` (#14181)

feat(data/zmod/quotient): More API for `orbit_zpowers_equiv` (#14181) This PR adds another `symm_apply` API lemma for `orbit_zpowers_equiv`, taking `(k : ℤ)` rather than `(k : zmod (minimal_period ((•) a) b))`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>