## Stream: maths

### Topic: Multiplication by n in an additive commutative group

#### Johan Commelin (May 14 2018 at 10:35):

Is this somewhere in mathlib?

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


#### Johannes Hölzl (May 14 2018 at 11:37):

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

Thanks!

#### Mario Carneiro (May 14 2018 at 18:16):

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

Last updated: May 18 2021 at 08:14 UTC