Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-31 04:59 a285049b

View on Github →

chore(algebra/group_hom): rename add_monoid.smul to nsmul (#2861) Also drop • as a notation for two smuls declared in this file, use •ℕ and •ℤ instead. This way one can immediately see that a lemma uses nsmul/gsmul, not has_scalar.smul.

Estimated changes

added theorem finset.sum_nsmul
deleted theorem finset.sum_smul'
added theorem commute.nsmul_left
added theorem commute.nsmul_nsmul
added theorem commute.nsmul_right
added theorem commute.nsmul_self
added theorem commute.self_nsmul
deleted theorem commute.self_smul
deleted theorem commute.self_smul_smul
deleted theorem commute.smul_left
deleted theorem commute.smul_right
deleted theorem commute.smul_self
deleted theorem commute.smul_smul
modified theorem add_gsmul
deleted theorem add_monoid.add_smul
deleted theorem add_monoid.mul_smul'
deleted theorem add_monoid.mul_smul
deleted theorem add_monoid.mul_smul_assoc
deleted theorem add_monoid.mul_smul_left
deleted theorem add_monoid.neg_smul
deleted theorem add_monoid.one_smul
deleted def add_monoid.smul
deleted theorem add_monoid.smul_add
deleted theorem add_monoid.smul_eq_mul'
deleted theorem add_monoid.smul_eq_mul
deleted theorem add_monoid.smul_le_smul
deleted theorem add_monoid.smul_neg_comm
deleted theorem add_monoid.smul_nonneg
deleted theorem add_monoid.smul_one
deleted theorem add_monoid.smul_sub
deleted theorem add_monoid.smul_zero
deleted theorem add_monoid.zero_smul
modified theorem add_monoid_hom.map_gsmul
deleted theorem add_monoid_hom.map_smul
added theorem add_nsmul
modified theorem add_one_gsmul
modified theorem bit0_gsmul
added theorem bit0_nsmul
deleted theorem bit0_smul
modified theorem bit1_gsmul
added theorem bit1_nsmul
deleted theorem bit1_smul
modified theorem gsmul_add_comm
modified theorem gsmul_coe_nat
modified theorem gsmul_mul'
modified theorem gsmul_mul
modified theorem gsmul_neg_succ
modified theorem gsmul_of_nat
modified theorem gsmul_one
modified theorem gsmul_zero
modified theorem list.sum_repeat
added theorem mul_nsmul'
added theorem mul_nsmul
added theorem mul_nsmul_assoc
added theorem mul_nsmul_left
added theorem nat.nsmul_eq_mul
deleted theorem nat.smul_eq_mul
modified theorem neg_gsmul
added theorem neg_nsmul
modified theorem neg_one_gsmul
added def nsmul
added theorem nsmul_add
added theorem nsmul_add_comm'
added theorem nsmul_add_comm
added theorem nsmul_eq_mul'
added theorem nsmul_eq_mul
added theorem nsmul_le_nsmul
added theorem nsmul_neg_comm
added theorem nsmul_nonneg
added theorem nsmul_one
added theorem nsmul_sub
added theorem nsmul_zero
added theorem of_add_nsmul
deleted theorem of_add_smul
modified theorem one_add_gsmul
modified theorem one_gsmul
added theorem one_nsmul
deleted theorem smul_add_comm'
deleted theorem smul_add_comm
added theorem succ_nsmul'
added theorem succ_nsmul
deleted theorem succ_smul'
deleted theorem succ_smul
added theorem two_nsmul
deleted theorem two_smul'
added theorem with_bot.coe_nsmul
deleted theorem with_bot.coe_smul
modified theorem zero_gsmul
added theorem zero_nsmul
added theorem semiconj_by.nsmul_left
deleted theorem semiconj_by.smul_left
deleted theorem semiconj_by.smul_right
deleted theorem semiconj_by.smul_smul
deleted theorem multiset.to_finset_smul
modified theorem finsupp.to_multiset_single
modified theorem multiset.count_smul
modified theorem multiset.sum_repeat
modified theorem polynomial.degree_pow_le
added theorem nnreal.nsmul_coe
deleted theorem nnreal.smul_coe
modified theorem multiples.self_mem
modified theorem multiples.zero_mem
modified def multiples
modified def tactic.abel.smul
modified def tactic.abel.smulg
modified def tactic.abel.term
modified def tactic.abel.termg