Commit 2024-05-13 09:51 d508ba88

View on Github →

chore: Move power lemmas earlier (#12736) Move a bunch of pow lemmas from Algebra.Group.Commute.Defs and Algebra.GroupPower.Basic to Algebra.Group.Defs and Algebra.Group.Basic with little to no changes to their proofs.

Estimated changes

modified theorem div_div_self'
added theorem div_pow
added theorem div_zpow
added theorem inv_pow
added theorem inv_pow_sub
added theorem inv_zpow'
added theorem inv_zpow
added theorem mul_pow
added theorem mul_pow_sub_one
added theorem mul_self_zpow
added theorem mul_zpow
added theorem mul_zpow_neg_one
added theorem mul_zpow_self
added theorem one_div_pow
added theorem one_div_zpow
added theorem one_zpow
added theorem pow_boole
added theorem pow_eq_pow_mod
added theorem pow_mul_pow_eq_one
added theorem pow_mul_pow_sub
added theorem pow_sub
added theorem pow_sub_mul_pow
added theorem pow_sub_one_mul
added theorem zpow_add
added theorem zpow_add_one
added theorem zpow_eq_zpow_emod'
added theorem zpow_eq_zpow_emod
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_neg
added theorem zpow_one_add
added theorem zpow_sub
added theorem zpow_sub_one
deleted theorem mul_inv_cancel_comm
deleted theorem mul_inv_cancel_comm_assoc
deleted theorem mul_pow_sub_one
deleted theorem pow_sub_one_mul
deleted theorem pow_succ'
modified theorem left_inv_eq_right_inv
added theorem mul_inv_cancel_comm
added theorem one_pow
added theorem pow_add
added theorem pow_mul'
added theorem pow_mul
added theorem pow_mul_comm'
added theorem pow_mul_comm
added theorem pow_one
added theorem pow_right_comm
added theorem pow_succ'
added theorem pow_three'
added theorem pow_three
added theorem pow_two
added theorem zpow_neg_coe_of_pos
added theorem zpow_neg_one
added theorem zpow_one
added theorem zpow_two
deleted theorem add_nsmul
deleted theorem div_pow
deleted theorem div_zpow
deleted theorem inv_pow
deleted theorem inv_pow_sub
deleted theorem inv_zpow'
deleted theorem inv_zpow
deleted theorem mul_pow
deleted theorem mul_self_zpow
deleted theorem mul_zpow
deleted theorem mul_zpow_neg_one
deleted theorem mul_zpow_self
deleted theorem nsmul_zero
deleted theorem one_div_pow
deleted theorem one_div_zpow
deleted theorem one_nsmul
deleted theorem one_pow
deleted theorem one_zpow
deleted theorem pow_add
deleted theorem pow_boole
deleted theorem pow_eq_pow_mod
deleted theorem pow_mul'
deleted theorem pow_mul
deleted theorem pow_mul_comm'
deleted theorem pow_mul_comm
deleted theorem pow_mul_pow_eq_one
deleted theorem pow_mul_pow_sub
deleted theorem pow_one
deleted theorem pow_right_comm
deleted theorem pow_sub
deleted theorem pow_sub_mul_pow
deleted theorem pow_three'
deleted theorem pow_three
deleted theorem pow_two
deleted theorem zpow_add
deleted theorem zpow_add_one
deleted theorem zpow_eq_zpow_emod'
deleted theorem zpow_eq_zpow_emod
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_neg
deleted theorem zpow_neg_coe_of_pos
deleted theorem zpow_neg_one
deleted theorem zpow_one
deleted theorem zpow_one_add
deleted theorem zpow_sub
deleted theorem zpow_sub_one
deleted theorem zpow_two