Tangent function

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.