Commit 2024-01-16 16:52 1564a327

View on Github →

chore: Move zpow lemmas (#9720) These lemmas can be proved much earlier with little to no change to their proofs. Part of #9411

Estimated changes

added theorem mul_self_zpow
added theorem mul_zpow_self
added theorem zpow_add
added theorem zpow_add_one
added theorem zpow_bit0'
added theorem zpow_bit0
added theorem zpow_bit1
added theorem zpow_induction_left
added theorem zpow_induction_right
added theorem zpow_mul'
added theorem zpow_mul
added theorem zpow_mul_comm
added theorem zpow_one_add
added theorem zpow_sub
added theorem zpow_sub_one
deleted theorem mul_self_zpow
deleted theorem mul_zpow_self
deleted theorem zpow_add
deleted theorem zpow_add_one
deleted theorem zpow_bit0'
deleted theorem zpow_bit0
deleted theorem zpow_bit0_neg
deleted theorem zpow_bit1
deleted theorem zpow_induction_left
deleted theorem zpow_induction_right
deleted theorem zpow_mul'
deleted theorem zpow_mul
deleted theorem zpow_mul_comm
deleted theorem zpow_one_add
deleted theorem zpow_sub
deleted theorem zpow_sub_one
added theorem zpow_bit0_neg