Zulip Chat Archive
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?
Adam Topaz (Sep 25 2020 at 16:34):
Chris Hughes (Sep 25 2020 at 17:06):
https://www.youtube.com/watch?v=ZPv1UV0rD8U
Kevin Buzzard (Sep 25 2020 at 17:31):
The fundamental period is 2*pi*I, right?
Johan Commelin (Sep 25 2020 at 17:31):
The lack of this definition is what is blocking us from doing complex analysis :rofl:
Last updated: Dec 20 2023 at 11:08 UTC