---
tag: 0V7E9KP6Q2
kind: definition
name: Square root function
msc: [26A09]
defines: 0E10E0NW9V
uses: [00KAFBR32E, 0TR9SR9FTB]
sources:
  - url: https://en.wikipedia.org/wiki/Square_root
    locator: Properties and uses
---

## Definition

For a real number $x \ge 0$, the square root $\sqrt{x}$ is the unique real number $y \ge 0$ with $y^2 = x$.
The square root function is the function $x \mapsto \sqrt{x}$ on $[0, \infty)$.

## Remarks

The number $y$ exists by the [[intermediate value theorem|00KAFBR32E]] for $t \mapsto t^2$. It is unique because $t^2$ is [[strictly increasing|0TR9SR9FTB]] on $[0, \infty)$.
The function is continuous and strictly increasing. It is differentiable on $(0, \infty)$, but not at $0$.
For $x > 0$, $\sqrt{x} = x^{1/2}$. Also $\sqrt{x^2} = |x|$ for every real $x$. Mathlib defines `Real.sqrt`, with $\sqrt{x} = 0$ for $x < 0$.

## Explanations

### L1 human

The square root of $x$ is the nonnegative number whose square is $x$.
For example, $\sqrt{9} = 3$, not $-3$.