Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-25 10:09 8e4ef23a

View on Github →

refactor(*): kill int multiplication diamonds (#7255) Insert a data field gsmul in add_comm_group containing a Z-action, and use it to make sure that all diamonds related to Z -actions disappear. Followup to #7084

Estimated changes

added def gpow_rec
added def gsmul_rec
deleted def gpow
modified theorem gpow_coe_nat
added theorem gpow_eq_pow
modified theorem gpow_neg_one
modified theorem gpow_neg_succ_of_nat
modified theorem gpow_of_nat
modified theorem gpow_one
modified theorem gpow_zero
deleted theorem group.gpow_eq_has_pow
deleted def gsmul
modified theorem gsmul_add
modified theorem gsmul_coe_nat
added theorem gsmul_eq_smul
modified theorem gsmul_neg
modified theorem gsmul_neg_succ_of_nat
modified theorem gsmul_of_nat
modified theorem gsmul_sub
modified theorem gsmul_zero
modified theorem neg_gsmul
modified theorem neg_one_gsmul
modified theorem of_mul_gpow
modified theorem one_gsmul
modified theorem zero_gsmul
modified theorem add_gsmul
modified theorem add_monoid_hom.map_gsmul
modified theorem add_one_gsmul
modified theorem bit0_gsmul
modified theorem bit0_mul
modified theorem bit1_gsmul
modified theorem bit1_mul
modified theorem gsmul_add_comm
modified theorem gsmul_eq_mul'
modified theorem gsmul_eq_mul
modified theorem gsmul_int_int
modified theorem gsmul_int_one
modified theorem gsmul_le_gsmul
modified theorem gsmul_le_gsmul_iff
modified theorem gsmul_lt_gsmul
modified theorem gsmul_lt_gsmul_iff
modified theorem gsmul_mul'
deleted theorem gsmul_mul
modified theorem gsmul_one
modified theorem gsmul_pos
modified theorem mul_bit0
modified theorem mul_bit1
added theorem mul_gsmul
modified theorem mul_gsmul_assoc
modified theorem mul_gsmul_left
modified theorem one_add_gsmul
modified theorem sub_gsmul
deleted def fpow
deleted theorem fpow_coe_nat
modified theorem fpow_neg_one
deleted theorem fpow_neg_succ_of_nat
deleted theorem fpow_of_nat
deleted theorem fpow_one
deleted theorem fpow_zero
deleted theorem gsmul_def
deleted theorem gsmul_eq_smul
modified theorem gsmul_eq_smul_cast
modified theorem int.smul_one_eq_coe
added theorem int_smul_eq_gsmul
modified theorem intermediate_field.pow_mem
modified theorem exists_gpow_eq_one
modified theorem exists_gsmul_eq_zero
modified theorem gsmul_eq_mod_add_order_of
modified theorem add_subgroup.coe_gsmul
modified def tactic.abel.smulg
modified def tactic.abel.termg