Scalar multiplication by ℕ and by R in a module

Stream: new members

[Luiz Kazuo Takei]

In a module M (that is, [Ring R] [AddCommGroup M] [Module R M]), we have two scalar multiplications: one by elements of ℕ and another one by elements of R.

Is there a theorem that says that those two scalar multiplications are the same (when viewing elements of ℕ as elements of R)? That is, how to complete the example below?

example [Ring R] [AddCommGroup M] [Module R M] (x : M) (n : ℕ) :
    n • x = (n:R) • x := sorry

[Robin Arnez]

docs#Nat.cast_smul_eq_nsmul​?

[Luiz Kazuo Takei]

Thanks @Robin Arnez !