## Stream: new members

### Topic: definition of tan

#### Benjamin Davidson (Jul 31 2020 at 17:33):

Hi everyone, I wanted to solicit your advice on some ideas I had regarding improving the definition of the tan function, which can essentially be broken down into 3 parts:
1) Proving ∀ (x:ℝ), cos x = 0 ↔ (∃ (n:ℕ), x = n*π + π/2)
2) Improve the precision of statements that currently use {x // cos x ≠ 0} (i.e. the continuity of tan) so that they instead use {x // ∃ (n:ℕ), x = n*π + π/2}ᶜ
3) Write a proof for the derivative of tan using the lemma described in (1)
Thanks!

#### Kevin Buzzard (Jul 31 2020 at 17:40):

We have cos_eq_zero_iff in analysis.special_functions.trigonometric.

#### Kevin Buzzard (Jul 31 2020 at 17:41):

n needs to be an integer, not a natural. Note that you're not improving the definition of tan, indeed you're not changing the definition of tan at all, you're proving theorems about the definition.

#### Heather Macbeth (Jul 31 2020 at 18:51):

The current lemma for continuity of tan has the statement

lemma continuous_tan : continuous (λ x : {x // cos x ≠ 0}, tan x)


and I think Ben is asking, would it be an improvement to change this statement to use {x // ∃ (n:ℕ), x = n*π + π/2}ᶜ instead of {x // cos x ≠ 0} ?

#### Eric Wieser (Aug 02 2020 at 10:41):

Presumably there is already a lemma which can translate one .property into the other?

#### Kevin Buzzard (Aug 02 2020 at 10:41):

cos_eq_zero_iff

Last updated: May 16 2021 at 05:21 UTC