isSquare

Mathlib.Data.Real.Sqrt

URI: https://scilib.ai/kg/mathlib#NNReal.isSquare

English

Every nonnegative real is a square: for all x ≥ 0, IsSquare(x).

Русский

Каждое неотрицательное число является квадратом: ∀x ≥ 0, IsSquare(x).

LaTeX

$$$\\forall x \\in \\mathbb{R}_{\\ge 0}, \\operatorname{IsSquare}(x)$$$

Lean4

@[simp]
theorem isSquare (x : ℝ≥0) : IsSquare x :=
  ⟨_, mul_self_sqrt _ |>.symm⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru