Commit 2023-12-16 07:33 9b2f0dca

View on Github →

chore: Nsmul -> NSMul, Zpow -> ZPow, etc (#9067) Normalising to naming convention rule number 6.

Estimated changes

modified theorem GradedMonoid.mk_smul_mk
added theorem SetLike.coe_GSMul
deleted theorem SetLike.coe_GSmul
added theorem prodXSubSMul.coeff
added theorem prodXSubSMul.eval
added theorem prodXSubSMul.monic
added theorem prodXSubSMul.smul
deleted theorem prodXSubSmul.coeff
deleted theorem prodXSubSmul.eval
deleted theorem prodXSubSmul.monic
deleted theorem prodXSubSmul.smul
added def Int.clogZPowGi
deleted def Int.clogZpowGi
added theorem finEquivZPowers_apply
deleted theorem finEquivZpowers_apply
deleted theorem zpowersEquivZpowers_apply
added def Dioph.DiophPFun
deleted def Dioph.DiophPfun
modified theorem Dioph.diophFn_iff_pFun
added theorem Dioph.diophPFun_comp1
added theorem Dioph.diophPFun_vec
deleted theorem Dioph.diophPfun_comp1
deleted theorem Dioph.diophPfun_vec
modified theorem Dioph.dom_dioph
modified theorem Dioph.xn_dioph
added theorem selfZPow_add
added theorem selfZPow_coe_nat
added theorem selfZPow_mul_neg
added theorem selfZPow_neg_coe_nat
added theorem selfZPow_neg_mul
added theorem selfZPow_of_neg
added theorem selfZPow_of_nonneg
added theorem selfZPow_of_nonpos
added theorem selfZPow_pow_sub
added theorem selfZPow_sub_cast_nat
added theorem selfZPow_zero
deleted theorem selfZpow_add
deleted theorem selfZpow_coe_nat
deleted theorem selfZpow_mul_neg
deleted theorem selfZpow_neg_coe_nat
deleted theorem selfZpow_neg_mul
deleted theorem selfZpow_of_neg
deleted theorem selfZpow_of_nonneg
deleted theorem selfZpow_of_nonpos
deleted theorem selfZpow_pow_sub
deleted theorem selfZpow_sub_cast_nat
deleted theorem selfZpow_zero
added def Set.Icc.addNSMul
added theorem Set.Icc.addNSMul_zero
deleted def Set.Icc.addNsmul
deleted theorem Set.Icc.addNsmul_eq_right
deleted theorem Set.Icc.addNsmul_zero
deleted theorem Set.Icc.monotone_addNsmul