Zulip Chat Archive

Stream: maths

Topic: Multiplication by n in an additive commutative group


view this post on Zulip 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

view this post on Zulip Johannes Hölzl (May 14 2018 at 11:37):

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

view this post on Zulip Johan Commelin (May 14 2018 at 11:49):

Thanks!

view this post on Zulip 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