feat(group_theory/subgroup/basic): zpowers_eq_bot (#14366) This PR adds a lemma zpowers_eq_bot.
zpowers_eq_bot