# Zulip Chat Archive

## 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)

What do you think about this? I would appreciate any critiques or suggestions.

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