---
tag: 06T0HS14PP
kind: definition
name: Tangent function
msc: [33B10]
defines: 05CG0S20S3
uses: [0WB57D9488]
sources:
  - url: https://en.wikipedia.org/wiki/Trigonometric_functions
    locator: Definitions in analysis
---

## Definition

The tangent function is defined by
$$\tan x = \frac{\sin x}{\cos x}$$
for all real $x$ with $\cos x \ne 0$, that is, for $x \ne \frac{\pi}{2} + k \pi$ with $k \in \mathbb{Z}$.

## Remarks

The function is odd and periodic with period $\pi$.
On $(-\pi/2, \pi/2)$ it is strictly increasing, and it maps this interval onto $\mathbb{R}$.
The related functions are $\cot x = \cos x / \sin x$, $\sec x = 1 / \cos x$ and $\csc x = 1 / \sin x$. Mathlib defines `Real.tan` with the value $0$ where $\cos x = 0$.

## Explanations

### L1 human

The tangent of an angle is the slope of the line through the origin at that angle.
It is undefined where this line is vertical.