Zulip Chat Archive

Stream: maths

Topic: de Moivre


view this post on Zulip Johan Commelin (Sep 24 2020 at 18:43):

Do we not yet have de Moivre in mathlib ? :shock: ??

view this post on Zulip Johan Commelin (Sep 24 2020 at 18:43):

I can't find it anywhere

view this post on Zulip Reid Barton (Sep 24 2020 at 18:44):

I found this with grep, does it answer the question?

17:
  title  : De Moivre’s Theorem
  decl   : complex.cos_add_sin_mul_I_pow
  author : Abhimanyu Pallavi Sudhir

view this post on Zulip Reid Barton (Sep 24 2020 at 18:45):

obviously the actual lemma should have a docstring with the name and not just 100.yaml

view this post on Zulip Johan Commelin (Sep 24 2020 at 18:47):

Thanks, I'll PR a docstring

view this post on Zulip Johan Commelin (Sep 24 2020 at 18:52):

#4242


Last updated: May 14 2021 at 19:21 UTC