Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-04-03 20:45 e655e4ea

View on Github →

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

Estimated changes