Multiplication by n in an additive commutative group

Stream: maths

[Johan Commelin]

Is this somewhere in mathlib?

definition mul_n {G : Type*} [add_comm_group G] (n : ℤ) (g : G) : G := n • g -- sorry

[Johannes Hölzl]

Its gsmul (generalized(?) scalar multiplication) in algebra.group_power

[Johan Commelin]

Thanks!

[Mario Carneiro]

the "g" stands for "group" in gsmul and gpow.