Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-28 02:37 9db72700

View on Github →

chore(*): rename gsmul to zsmul and gmultiples to zmultiples (#10010) This is consistent with an earlier rename from gpow to zpow.

Estimated changes

deleted theorem subalgebra.gsmul_mem
added theorem subalgebra.zsmul_mem
deleted theorem finset.gsmul_sum
added theorem finset.zsmul_sum
deleted def gsmul_rec
added def zsmul_rec
deleted theorem of_add_gsmul
added theorem of_add_zsmul
deleted theorem abs_gsmul
added theorem abs_zsmul
deleted theorem add_gsmul
deleted theorem add_monoid_hom.map_gsmul
deleted theorem add_one_gsmul
added theorem add_one_zsmul
added theorem add_zsmul
deleted theorem bit0_gsmul
added theorem bit0_zsmul
deleted theorem bit1_gsmul
added theorem bit1_zsmul
deleted def gmultiples_add_hom
deleted theorem gmultiples_add_hom_apply
deleted def gmultiples_hom
deleted theorem gmultiples_hom_apply
deleted theorem gmultiples_hom_symm_apply
deleted theorem gsmul_add_comm
deleted theorem gsmul_eq_gsmul_iff'
deleted theorem gsmul_eq_mul'
deleted theorem gsmul_eq_mul
deleted theorem gsmul_int_int
deleted theorem gsmul_int_one
deleted theorem gsmul_le_gsmul'
deleted theorem gsmul_le_gsmul
deleted theorem gsmul_le_gsmul_iff'
deleted theorem gsmul_le_gsmul_iff
deleted theorem gsmul_lt_gsmul'
deleted theorem gsmul_lt_gsmul
deleted theorem gsmul_lt_gsmul_iff'
deleted theorem gsmul_lt_gsmul_iff
deleted theorem gsmul_mono_left
deleted theorem gsmul_mono_right
deleted theorem gsmul_mul'
deleted theorem gsmul_one
deleted theorem gsmul_pos
deleted theorem gsmul_right_inj
deleted theorem gsmul_right_injective
deleted theorem gsmul_strict_mono_left
deleted theorem gsmul_strict_mono_right
deleted theorem mul_gsmul
deleted theorem mul_gsmul_assoc
deleted theorem mul_gsmul_left
added theorem mul_zsmul
added theorem mul_zsmul_assoc
added theorem mul_zsmul_left
deleted theorem one_add_gsmul
added theorem one_add_zsmul
deleted theorem sub_gsmul
added theorem sub_zsmul
added def zmultiples_hom
added theorem zmultiples_hom_apply
added theorem zsmul_add_comm
added theorem zsmul_eq_mul'
added theorem zsmul_eq_mul
added theorem zsmul_eq_zsmul_iff'
added theorem zsmul_int_int
added theorem zsmul_int_one
added theorem zsmul_le_zsmul'
added theorem zsmul_le_zsmul
added theorem zsmul_le_zsmul_iff'
added theorem zsmul_le_zsmul_iff
added theorem zsmul_lt_zsmul'
added theorem zsmul_lt_zsmul
added theorem zsmul_lt_zsmul_iff'
added theorem zsmul_lt_zsmul_iff
added theorem zsmul_mono_left
added theorem zsmul_mono_right
added theorem zsmul_mul'
added theorem zsmul_one
added theorem zsmul_pos
added theorem zsmul_right_inj
added theorem zsmul_right_injective
added theorem zsmul_strict_mono_left
deleted theorem gsmul_lie
deleted theorem lie_gsmul
added theorem lie_zsmul
added theorem zsmul_lie
deleted theorem gsmul_eq_smul_cast
deleted theorem int_smul_eq_gsmul
added theorem int_smul_eq_zsmul
added theorem zsmul_eq_smul_cast
deleted theorem function.periodic.gsmul
deleted theorem star_gsmul
added theorem star_zsmul
deleted theorem nnnorm_gsmul_le
added theorem nnnorm_zsmul_le
deleted theorem norm_gsmul_le
added theorem norm_zsmul_le
deleted theorem subfield.gsmul_mem
added theorem subfield.zsmul_mem
deleted theorem exists_gsmul_eq_zero
added theorem exists_zsmul_eq_zero
deleted theorem gsmul_eq_mod_add_order_of
deleted theorem multiples_eq_gmultiples
deleted theorem add_subgroup.coe_gsmul
added theorem add_subgroup.coe_zsmul
deleted theorem int.mem_gmultiples_iff
added theorem int.mem_zmultiples_iff
deleted theorem int.gmultiples_nat_abs
added theorem int.zmultiples_nat_abs
deleted theorem is_integral.gsmul
added theorem is_integral.zsmul
deleted theorem subring.gsmul_mem
added theorem subring.zsmul_mem
deleted theorem tactic.abel.unfold_gsmul