Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-09 14:39 bd0a555d

View on Github →

fix(algebra/group_power): remove has_smul This was causing notation overload problems with module smul

Estimated changes

modified theorem add_monoid.mul_smul'
modified theorem add_monoid.neg_smul
modified theorem add_monoid.smul_add
modified theorem add_monoid.smul_neg_comm
modified theorem add_monoid.smul_nonneg
modified theorem gpow_coe_nat
modified theorem gpow_neg_succ
modified theorem gpow_of_nat
modified theorem gsmul_add_comm
modified theorem gsmul_coe_nat
modified theorem gsmul_eq_mul'
modified theorem gsmul_eq_mul
modified theorem gsmul_neg_succ
modified theorem gsmul_of_nat
modified theorem mul_gsmul_assoc
modified theorem mul_gsmul_left