mathlib

e655e4ea - feat(algebra/group_power/lemmas): Induction principle for powers (#18668)

feat(algebra/group_power/lemmas): Induction principle for powers (#18668) A property holds for all powers of `g` if it is holds for `1` and is preserved under multiplication and division by `g`. Also rename `subgroup.zpowers_subset`/`add_subgroup.zmultiples_subset` to `subgroup.zpowers_le_of_mem`/`add_subgroup.zmultiples_le_of_mem` because there is no `⊆` in the statement. The motivation is the Cauchy-Davenport theorem: https://github.com/leanprover-community/mathlib/blob/321b67021163ac504c6cfa35d5678a47b357869d/src/combinatorics/additive/cauchy_davenport.lean#L176-L181