Commit 2022-04-26 09:51 4c6b3737
View on Github →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.
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.