Commit 2021-12-27 18:57 294e78e7

View on Github →

feat(algebra/group_with_zero/power): With zero lemmas (#11051) This proves the group_with_zero variant of some lemmas and moves lemmas from algebra.group_power.basic to algebra.group_with_zero.power.

Estimated changes

Modified src/algebra/group_power/basic.lean

Modified src/algebra/group_with_zero/power.lean

deleted theorem fzero_pow_eq

added theorem inv_pow_sub_of_lt

added theorem inv_pow_sub₀

added theorem mul_zpow_neg_one₀

modified theorem mul_zpow₀

added theorem pow_sub_of_lt

added theorem zero_zpow_eq

added def zpow_group_hom₀

added theorem zpow_neg_one₀