nsmul_eq_mul

Stream: general

[Sebastien Gouezel]

The lemma nsmul_eq_mul states that

theorem nsmul_eq_mul [semiring R] (n : ℕ) (a : R) : n •ℕ a = n * a :=
by rw [nsmul_eq_mul', nat.mul_cast_comm]

Since I never care about the weird integer multiplication (and I always take too long a time to find the name of this lemma), I would like to put a simp attribute on it, but maybe in other domains this would be a bad idea, so I thought I would ask here first. I uploaded a branch with the modification, and the linter complains about a lot of lemmas that are not any more in simp normal form (which should be expected), and about several simp lemmas that can now be proved automatically and therefore should not have the simp attribute any more. See https://github.com/leanprover-community/mathlib/runs/746885094

[Johan Commelin]

I guess it takes a lot of effort to fix this, but in principle I like it a a simp lemma

[Mario Carneiro]

I think this is fine as a simp lemma

[Mario Carneiro]

for semirings and up we pretty much always want to use multiplication in place of scalar multiple

[Sebastien Gouezel]

#2983