## Stream: maths

### Topic: 2 * pi * I

#### Johan Commelin (Sep 25 2020 at 16:12):

Does it make sense to create a definition two_pi_I := 2 * pi * I? That might make it easier to cancel it, or move it through equations with assoc and comm.

#### Adam Topaz (Sep 25 2020 at 16:22):

two_pi_I is really an atomic object from the motivic point of view anyway...

#### Adam Topaz (Sep 25 2020 at 16:31):

Should pi_I also be defined?

#### Chris Hughes (Sep 25 2020 at 17:06):

The fundamental period is 2*pi*I, right?