lean_workbook_plus_20966

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

The equation $\sqrt{a^2} = a$ is true only if a is nonnegative. If we do not know the sign of $\color[rgb]{0.11,0.21,0.37}a$ , then we cannot simplify $\sqrt{a^2}$ to $a$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_20966  (a : ℝ) :
  Real.sqrt (a^2) = a ↔ 0 ≤ a   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph