-
Notifications
You must be signed in to change notification settings - Fork 234
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(Trigonometric): add Complex.tan_eq_zero_iff'
#9877
Conversation
This version assumes that the cosine is not zero.
iff this number is equal to `k * π / 2` for an integer `k`. | ||
|
||
Note that this lemma takes into account that we use zero as the junk value for division by zero. | ||
See also `Complex.tan_eq_zero_iff'`. -/ | ||
theorem tan_eq_zero_iff {θ : ℂ} : tan θ = 0 ↔ ∃ k : ℤ, θ = k * π / 2 := by |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could you take this occasion to swap the right hand side to k * π / 2 = θ
? Same thing in the next lemma.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done (for tangent, not for other trig functions).
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…y/mathlib4 into YK-tan-eq-zero
bors r+ |
This version assumes that the cosine is not zero.
Pull request successfully merged into master. Build succeeded: |
Complex.tan_eq_zero_iff'
Complex.tan_eq_zero_iff'
This version assumes that the cosine is not zero.