Zulip Chat Archive

Stream: maths

Topic: de Moivre

Johan Commelin (Sep 24 2020 at 18:43):

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

Johan Commelin (Sep 24 2020 at 18:43):

I can't find it anywhere

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

Reid Barton (Sep 24 2020 at 18:45):

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

Johan Commelin (Sep 24 2020 at 18:47):

Thanks, I'll PR a docstring

Johan Commelin (Sep 24 2020 at 18:52):

#4242

Last updated: Dec 20 2023 at 11:08 UTC