Commit 2022-12-19 11:23 1bec125b

View on Github →

feat port Algebra.GroupPower.Lemmas (#1055) aba57d4d3dae35460225919dcd82fe91355162f9

depends on #1043
depends on #1050

Estimated changes

Modified Mathlib/Algebra/Group/Basic.lean

added theorem bit0_neg

Modified Mathlib/Algebra/GroupPower/Lemmas.lean

added theorem AddMonoidHom.apply_int

added theorem AddMonoidHom.apply_nat

added theorem Commute.cast_int_left

added theorem Commute.cast_int_mul_cast_int_mul

added theorem Commute.cast_int_mul_left

added theorem Commute.cast_int_mul_right

added theorem Commute.cast_int_mul_self

added theorem Commute.cast_int_right

added theorem Commute.cast_nat_mul_cast_nat_mul

added theorem Commute.cast_nat_mul_left

added theorem Commute.cast_nat_mul_right

added theorem Commute.cast_nat_mul_self

added theorem Commute.self_cast_int_mul

added theorem Commute.self_cast_int_mul_cast_int_mul

added theorem Commute.self_cast_nat_mul

added theorem Commute.self_cast_nat_mul_cast_nat_mul

added theorem Commute.units_zpow_left

added theorem Commute.units_zpow_right

added theorem Int.abs_le_self_sq

modified theorem Int.cast_pow

added theorem Int.coe_nat_pow

added theorem Int.le_self_sq

added theorem Int.nat_abs_pow

added theorem Int.nat_abs_sq'

added theorem Int.nat_abs_sq

added theorem Int.of_add_mul

added theorem Int.pow_right_injective

added theorem Int.to_add_pow

added theorem Int.to_add_zpow

added theorem IsUnit.pow

added theorem MonoidHom.apply_mint

added theorem MonoidHom.apply_mnat

added theorem MonoidHom.ext_mnat

added theorem MulOpposite.op_pow

added theorem MulOpposite.op_zpow

added theorem MulOpposite.unop_pow

added theorem MulOpposite.unop_zpow

modified theorem Nat.cast_pow

added theorem Nat.of_add_mul

added theorem Nat.to_add_pow

added theorem SemiconjBy.cast_int_mul_cast_int_mul

added theorem SemiconjBy.cast_int_mul_left

added theorem SemiconjBy.cast_int_mul_right

added theorem SemiconjBy.cast_nat_mul_cast_nat_mul

added theorem SemiconjBy.cast_nat_mul_left

added theorem SemiconjBy.cast_nat_mul_right

added theorem SemiconjBy.units_zpow_right

added theorem Units.conj_pow'

added theorem Units.conj_pow

added def Units.ofPow

added def Units.ofPowEqOne

added theorem Units.pow_of_pow_eq_one

added theorem WithBot.coe_nsmul

added theorem abs_add_eq_add_abs_iff

added theorem abs_add_eq_add_abs_le

added theorem abs_nsmul

added theorem abs_pow

added theorem abs_zsmul

added theorem bit0_mul

added theorem bit1_mul

added theorem inv_of_pow

added def invertibleOfPowEqOne

added theorem is_unit_of_pow_eq_one

added theorem is_unit_pow_iff

added theorem is_unit_pow_succ_iff

added theorem mul_bit0

added theorem mul_bit1

added theorem mul_self_zpow

added theorem mul_zpow_self

added def multiplesAddHom

added theorem multiplesAddHom_apply

added def multiplesHom

added theorem multiples_add_hom_symm_apply

added theorem multiples_hom_apply

added theorem multiples_hom_symm_apply

added theorem neg_one_pow_eq_pow_mod_two

modified theorem nsmul_eq_mul'

modified theorem nsmul_eq_mul

added theorem nsmul_one

added theorem one_add_mul_le_pow'

added theorem one_add_mul_le_pow

added theorem one_add_mul_sub_le_pow

added theorem one_lt_zpow'

added theorem pow_bit1_neg_iff

added theorem pow_bit1_nonneg_iff

added theorem pow_bit1_nonpos_iff

added theorem pow_bit1_pos_iff

added theorem pow_le_of_le_one

added theorem pow_le_pow_of_le_one

added theorem pow_le_pow_of_le_one_aux

added def powersHom

added def powersMulHom

added theorem powers_hom_apply

added theorem powers_hom_symm_apply

added theorem powers_mul_hom_apply

added theorem powers_mul_hom_symm_apply

added theorem sign_cases_of_C_mul_pow_nonneg

added theorem smul_pow'

added theorem smul_pow

added theorem sq_le

added theorem strict_mono_pow_bit1

added def zmultiplesAddHom

added def zmultiplesHom

added theorem zmultiples_add_hom_apply

added theorem zmultiples_add_hom_symm_apply

added theorem zmultiples_hom_apply

added theorem zmultiples_hom_symm_apply

added theorem zpow_add

added theorem zpow_add_one

added theorem zpow_bit0'

added theorem zpow_bit0

added theorem zpow_bit0_neg

added theorem zpow_bit1

added theorem zpow_eq_zpow_iff'

added theorem zpow_le_zpow'

added theorem zpow_le_zpow

added theorem zpow_le_zpow_iff'

added theorem zpow_le_zpow_iff

added theorem zpow_left_inj

added theorem zpow_left_injective

added theorem zpow_lt_zpow'

added theorem zpow_lt_zpow

added theorem zpow_lt_zpow_iff'

added theorem zpow_lt_zpow_iff

added theorem zpow_mono_left

added theorem zpow_mono_right

added theorem zpow_mul'

added theorem zpow_mul

added theorem zpow_mul_comm

added theorem zpow_one_add

added theorem zpow_strict_mono_left

added theorem zpow_strict_mono_right

added theorem zpow_sub

added theorem zpow_sub_one

added def zpowersHom

added def zpowersMulHom

added theorem zpowers_hom_apply

added theorem zpowers_hom_symm_apply

added theorem zpowers_mul_hom_apply

added theorem zpowers_mul_hom_symm_apply

added theorem zsmul_eq_mul'

added theorem zsmul_eq_mul

added theorem zsmul_int_int

added theorem zsmul_int_one

added theorem zsmul_one

Modified Mathlib/Algebra/Invertible.lean

Modified Mathlib/Data/Int/Basic.lean