Skip to content

Instantly share code, notes, and snippets.

@ChrisHughes24

ChrisHughes24/argtwitter

Created November 17, 2020 22:31
Show Gist options
  • Save ChrisHughes24/c3a0eee2ae269a922c07d8cd9b9577d4 to your computer and use it in GitHub Desktop.
Save ChrisHughes24/c3a0eee2ae269a922c07d8cd9b9577d4 to your computer and use it in GitHub Desktop.
Download ZIP
Proof of some problem in a tweet
Raw
argtwitter
import analysis.special_functions.trigonometric
open complex real
example (θ φ : ℝ) (h1 : θ ≤ pi) (h2 : -pi < θ)
(h3 : 0 < cos φ): arg (exp (I * θ) * cos φ) = θ :=
by rw [mul_comm, ← of_real_cos, arg_real_mul _ h3, mul_comm, exp_mul_I,
arg_cos_add_sin_mul_I h2 h1]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment