mathlib

4c6b3737 - feat(group_theory/subgroup/basic): `zpowers_le` (#13693)

feat(group_theory/subgroup/basic): `zpowers_le` (#13693) This PR adds a lemma `zpowers_le : zpowers g ≤ H ↔ g ∈ H`. I also fixed the `to_additive` name of a lemma from a previous PR.