Commit 2024-01-31 13:54 a05375f7

View on Github →

feat(Trigonometric): add Complex.tan_eq_zero_iff' (#9877) This version assumes that the cosine is not zero.

Estimated changes

deleted theorem Real.tan_eq_zero_iff
deleted theorem Real.tan_ne_zero_iff
modified theorem Complex.tan_eq_zero_iff
modified theorem Complex.tan_ne_zero_iff
added theorem Real.tan_eq_zero_iff'
added theorem Real.tan_eq_zero_iff
added theorem Real.tan_ne_zero_iff