grind provides multiplication by Nat

Stream: general

[Yaël Dillies]

docs#Lean.Grind.NatModule.nsmul is registered as an instance of HMul ℕ M M instead of SMul ℕ M, which means that you can end up writing an expression for which there is no API!

import Mathlib.Algebra.Group.Basic

variable {M : Type*} [AddCommMonoid M]

lemma foo (m : M) : 2 * m = m + m := two_nsmul _ -- definitely abusing defeq

[Yaël Dillies]

Would core be happy to change this to SMul?

[Kim Morrison]

It's already done.

[Yaël Dillies]

Is it? I see the same on master

[Markus Himmel]

lean4#10095