sqrt — Mathlib

English

For any integer n, sqrt(n^2) equals the absolute value |n|.

Русский

Для любого целого n выполнено: sqrt(n^2) = |n|.

LaTeX

$$$\sqrt{n^2} = |n|$$$

Lean4

/-- `sqrt z` is the square root of an integer `z`. If `z` is positive, it returns the largest
integer `r` such that `r * r ≤ n`. If it is negative, it returns `0`. For example, `sqrt (-1) = 0`,
`sqrt 1 = 1`, `sqrt 2 = 1` -/
@[pp_nodot]
def sqrt (z : ℤ) : ℤ :=
  Nat.sqrt <| Int.toNat z

Похожие утверждения