Commit 2022-12-07 23:03 3ffbf780

View on Github →

feat : port Algebra.GroupPower.Basic (#874) mathlib3 SHA: 9b2660e1b25419042c8da10bf411aa3c67f14383

Estimated changes

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 SemiconjBy.zpow_right
modified theorem add_nsmul
added theorem div_pow
added theorem div_zpow
added theorem dvd_pow
added theorem dvd_pow_self
added theorem inv_pow
added theorem inv_pow_sub
added theorem inv_zpow'
added theorem inv_zpow
added theorem ite_pow
added theorem mul_zpow
added theorem mul_zpow_neg_one
modified theorem nsmul_zero
added theorem ofAdd_nsmul
added theorem ofAdd_zsmul
added theorem ofMul_pow
added theorem ofMul_zpow
added theorem one_div_pow
added theorem one_div_zpow
modified theorem one_nsmul
modified theorem one_pow
added theorem one_zpow
added def powMonoidHom
added theorem pow_bit0'
added theorem pow_bit0
added theorem pow_bit1'
added theorem pow_bit1
added theorem pow_boole
added theorem pow_dvd_pow
added theorem pow_eq_pow_mod
added theorem pow_inv_comm
added theorem pow_ite
added theorem pow_mul'
added theorem pow_mul_comm'
added theorem pow_mul_comm
added theorem pow_mul_pow_eq_one
added theorem pow_mul_pow_sub
added theorem pow_right_comm
added theorem pow_sub
added theorem pow_sub_mul_pow
added theorem pow_three'
added theorem pow_three
added theorem pow_two
added def zpowGroupHom
added theorem zpow_neg
added theorem zpow_neg_coe_of_pos
added theorem zpow_neg_one
added theorem zpow_one
added theorem zpow_two