Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-17 00:02 737784ef

View on Github →

refactor(algebra/{group_power/{basic,lemmas},group_with_zero/power}): Generalize lemmas to division monoids (#14102) Generalize group and group_with_zero lemmas about zpow to division_monoid. Lemmas are renamed because one of the group or group_with_zero name has to go. It's just a matter of removing the suffixed ₀. Lemma renames

Estimated changes

deleted theorem zpow_bit0_neg
added theorem bit0_neg
deleted theorem commute.mul_zpow
added theorem div_pow
modified theorem div_zpow
modified theorem inv_pow
modified theorem inv_pow_sub
added theorem inv_zpow'
modified theorem inv_zpow
modified theorem mul_zpow
modified theorem mul_zpow_neg_one
added theorem one_div_pow
added theorem one_div_zpow
modified theorem one_zpow
modified theorem pow_inv_comm
modified theorem pow_sub
modified def zpow_group_hom
modified theorem zpow_neg
added theorem zpow_bit0'
modified theorem zpow_bit0
added theorem zpow_bit0_neg
modified theorem zpow_mul'
modified theorem zpow_mul
modified theorem zpow_mul_comm
deleted theorem commute.mul_zpow₀
deleted theorem div_pow
deleted theorem div_zpow₀
deleted theorem inv_pow₀
deleted theorem inv_zpow'
deleted theorem inv_zpow₀
deleted theorem mul_zpow_neg_one₀
deleted theorem mul_zpow₀
deleted theorem one_div_pow
deleted theorem one_div_zpow
deleted theorem one_zpow₀
deleted theorem zpow_bit0'
deleted theorem zpow_bit0₀
deleted def zpow_group_hom₀
deleted theorem zpow_mul₀'
deleted theorem zpow_mul₀
deleted theorem zpow_neg_one₀
deleted theorem zpow_neg₀
modified theorem even.neg_one_zpow
modified theorem odd.neg_one_zpow