Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-11-23 22:09 c03c16d6

View on Github →

feat(algebra/group_power): remove overloaded ^ notation, add smul

Estimated changes

deleted theorem inv_comm_of_comm
added theorem inv_comm_of_comm
added theorem add_monoid.add_smul
added theorem add_monoid.neg_smul
added theorem add_monoid.smul_mul
added theorem add_monoid.smul_one
added theorem add_monoid.zero_smul
deleted theorem has_pow_nat_eq_pow_nat
added theorem list.sum_repeat
modified def monoid.pow
added theorem nat.pow_eq_pow
deleted theorem nat.pow_eq_pow_nat
deleted def pow_int
modified theorem pow_inv_comm
deleted def pow_nat
modified theorem pow_one
modified theorem pow_zero
added theorem smul_bit1
added theorem smul_succ'
added theorem smul_succ