Commit 2023-04-12 19:26 f8369997

View on Github →

feat: Induction principle for powers (#3278) https://github.com/leanprover-community/mathlib/pull/18668

Estimated changes

Modified Mathlib/Algebra/GroupPower/Lemmas.lean

added theorem zpow_induction_left

added theorem zpow_induction_right

Modified Mathlib/GroupTheory/Subgroup/Pointwise.lean

Modified Mathlib/GroupTheory/Subgroup/Zpowers.lean

added theorem Subgroup.coe_zpowers

added theorem Subgroup.zpowers_ne_bot

deleted theorem Subgroup.zpowers_subset

Modified Mathlib/GroupTheory/Submonoid/Membership.lean

added theorem Submonoid.coe_powers

Modified Mathlib/RingTheory/Int/Basic.lean