Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-17 09:07 b42e5687

View on Github →

chore(algebra/group_power): rename type vars, minor cleanup (#1997) The only non-BC change should be removing is_group_hom.map_gpow/is_add_group_hom.map_gsmulin favor ofmonoid_hom.map_gpow`.

Estimated changes

modified theorem abs_neg_one_pow
modified theorem add_gsmul
modified theorem add_monoid.add_smul
modified theorem add_monoid.mul_smul'
modified theorem add_monoid.mul_smul
modified theorem add_monoid.mul_smul_assoc
modified theorem add_monoid.mul_smul_left
modified theorem add_monoid.neg_smul
modified theorem add_monoid.one_smul
modified def add_monoid.smul
modified theorem add_monoid.smul_add
modified theorem add_monoid.smul_eq_mul'
modified theorem add_monoid.smul_eq_mul
modified theorem add_monoid.smul_le_smul
modified theorem add_monoid.smul_neg_comm
modified theorem add_monoid.smul_nonneg
modified theorem add_monoid.smul_one
modified theorem add_monoid.smul_sub
modified theorem add_monoid.smul_zero
modified theorem add_monoid.zero_smul
modified theorem add_monoid_hom.map_gsmul
modified theorem add_monoid_hom.map_smul
modified theorem add_one_gsmul
modified theorem bit0_gsmul
modified theorem bit0_smul
modified theorem bit1_gsmul
modified theorem bit1_smul
modified theorem div_pow
modified theorem division_ring.inv_pow
modified def gpow
modified theorem gpow_add
modified theorem gpow_add_one
modified theorem gpow_bit0
modified theorem gpow_bit1
modified theorem gpow_coe_nat
modified theorem gpow_mul'
modified theorem gpow_mul
modified theorem gpow_mul_comm
modified theorem gpow_neg
modified theorem gpow_neg_one
modified theorem gpow_neg_succ
modified theorem gpow_of_nat
modified theorem gpow_one
modified theorem gpow_one_add
modified theorem gpow_zero
modified def gsmul
modified theorem gsmul_add
modified theorem gsmul_add_comm
modified theorem gsmul_coe_nat
modified theorem gsmul_eq_mul'
modified theorem gsmul_eq_mul
modified theorem gsmul_mul'
modified theorem gsmul_mul
modified theorem gsmul_neg
modified theorem gsmul_neg_succ
modified theorem gsmul_of_nat
modified theorem gsmul_one
modified theorem gsmul_sub
modified theorem gsmul_zero
modified theorem int.cast_pow
modified theorem inv_gpow
modified theorem inv_pow'
modified theorem inv_pow
deleted theorem is_add_group_hom.gsmul
deleted theorem is_add_group_hom.map_smul
modified theorem is_add_monoid_hom.map_smul
deleted theorem is_group_hom.map_gpow
deleted theorem is_group_hom.map_pow
modified theorem is_monoid_hom.map_pow
modified theorem is_semiring_hom.map_pow
modified theorem list.prod_repeat
modified theorem list.sum_repeat
modified theorem lt_of_pow_lt_pow
modified def monoid.pow
modified theorem monoid_hom.map_gpow
modified theorem monoid_hom.map_pow
modified theorem mul_gpow
modified theorem mul_gsmul_assoc
modified theorem mul_gsmul_left
modified theorem mul_pow
modified theorem nat.cast_pow
modified theorem neg_gsmul
modified theorem neg_one_gsmul
modified theorem neg_one_pow_eq_or
modified theorem neg_one_pow_eq_pow_mod_two
modified theorem one_add_gsmul
modified theorem one_add_mul_le_pow'
modified theorem one_add_mul_le_pow
modified theorem one_add_sub_mul_le_pow
modified theorem one_div_pow
modified theorem one_gpow
modified theorem one_gsmul
modified theorem one_le_pow_of_one_le
modified theorem one_pow
modified theorem pow_abs
modified theorem pow_add
modified theorem pow_bit0
modified theorem pow_bit1
modified theorem pow_div
modified theorem pow_dvd_pow
modified theorem pow_eq_zero
modified theorem pow_inv
modified theorem pow_inv_comm
modified theorem pow_le_one
modified theorem pow_le_pow
modified theorem pow_le_pow_of_le_left
modified theorem pow_le_pow_of_le_one
modified theorem pow_lt_pow
modified theorem pow_lt_pow_of_lt_left
modified theorem pow_lt_pow_of_lt_one
modified theorem pow_mul'
modified theorem pow_mul
modified theorem pow_mul_comm'
modified theorem pow_mul_comm
modified theorem pow_ne_zero
modified theorem pow_nonneg
modified theorem pow_one
modified theorem pow_pos
modified theorem pow_right_inj
modified theorem pow_sub
modified theorem pow_succ'
modified theorem pow_succ
modified theorem pow_two
modified theorem pow_two_nonneg
modified theorem pow_zero
modified theorem ring_hom.map_pow
modified theorem smul_add_comm'
modified theorem smul_add_comm
modified theorem sq_sub_sq
modified theorem succ_smul'
modified theorem succ_smul
modified theorem two_smul
modified theorem units.coe_pow
modified theorem with_bot.coe_smul
modified theorem zero_gsmul
modified theorem zero_pow
modified theorem real.angle.coe_gsmul
added theorem real.angle.coe_smul