mathlib3
4e1558bf - chore(algebra/group_power): simp attribute on nsmul_eq_mul and gsmul_eq_mul (#2983)

Commit
5 years ago
chore(algebra/group_power): simp attribute on nsmul_eq_mul and gsmul_eq_mul (#2983) Also fix the resulting lint failures, corresponding to the fact that several lemmas are not in simp normal form any more.
Author
Parents
Loading