Commit 2024-05-18 16:15 73a3870c

View on Github →

chore: Delete Algebra.GroupPower.Basic, Algebra.GroupWithZero.Bitwise (#11855) The entire Algebra.GroupPower folder is problematic in that it treats pow as an advanced subject while the rest of mathlib wants to treat it as a primitive. As such, its existence is an obstacle to developing the theory of pow transversally. This PR scatters the lemmas in Algebra.GroupPower.Basic to earlier files and deletes it. Also delete Algebra.GroupWithZero.Bitwise whose lemmas are completely deprecated (and hard to rehome). See #9411 for previous work.

Estimated changes

deleted theorem zpow_bit1_neg
added theorem Commute.self_zpow
added theorem Commute.zpow_left
added theorem Commute.zpow_right
added theorem Commute.zpow_self
added theorem Commute.zpow_zpow
added theorem Commute.zpow_zpow_self
added theorem pow_inv_comm
added theorem Commute.mul_pow
modified def Commute
modified theorem commute_iff_eq
added theorem pow_bit0'
added theorem pow_bit0
added theorem pow_bit1'
added theorem pow_bit1
added theorem SemiconjBy.zpow_right
deleted theorem Commute.mul_pow
deleted theorem Commute.self_zpow
deleted theorem Commute.zpow_left
deleted theorem Commute.zpow_right
deleted theorem Commute.zpow_self
deleted theorem Commute.zpow_zpow
deleted theorem Commute.zpow_zpow_self
deleted theorem SemiconjBy.zpow_right
deleted theorem pow_bit0'
deleted theorem pow_bit0
deleted theorem pow_bit1'
deleted theorem pow_bit1
deleted theorem pow_inv_comm
deleted theorem zpow_bit0'
deleted theorem zpow_bit0
deleted theorem zpow_bit1
deleted theorem zpow_bit0_neg
deleted theorem zpow_bit1'
deleted theorem zpow_bit1₀
modified theorem Odd.zpow_pos_iff
deleted theorem zpow_bit0_nonneg
deleted theorem zpow_bit0_pos
deleted theorem zpow_bit0_pos_iff
deleted theorem zpow_bit1_neg_iff
deleted theorem zpow_bit1_nonneg_iff
deleted theorem zpow_bit1_nonpos_iff
deleted theorem zpow_bit1_pos_iff
modified theorem zpow_neg_two_nonneg
modified theorem zpow_two_nonneg
modified theorem zpow_two_pos_of_ne_zero
deleted theorem Complex.I_zpow_bit0
deleted theorem Complex.I_zpow_bit1