Complex.arg_pow_coe_angle?

Stream: Is there code for X?

[Weiyi Wang]

Maybe I just missed it but is there a theorem like the following?

theorem Complex.arg_pow_coe_angle {x : ℂ} {n: ℕ}  : ((x ^ n).arg : Real.Angle) = n • (x.arg : Real.Angle)

I see there is Complex.arg_mul_coe_angle but I am surprised there is no pow version

[Ruben Van de Velde]

Seems like something reasonable to add

[Eric Wieser]

For zpow too

[Weiyi Wang]

Guess it is time for me to try making some contribution https://github.com/leanprover-community/mathlib4/pull/22738

[Ruben Van de Velde]

Unfortunately we cannot accept pull requests from a fork; you'll need to request write access to the main repository

[Weiyi Wang]

I see. Where do I do that?

[Jeremy Tan]

#mathlib4 > github permission @Weiyi Wang

[Kevin Buzzard]

A detailed description of the workflow is here. You could start by adding your github userid to your Zulip profile.

[Weiyi Wang]

Thanks! Let me fix it

[Kevin Buzzard]

OK I sent you an invitation so you don't need to post in the thread linked to above. When you re-make the PR from a branch can you write {n : ℕ} instead of {n: ℕ} and similarly with the integer version? We don't yet have a linter to pick up on these things.