not_isSquare_of_neg

Mathlib.Algebra.Order.Ring.Basic

URI: https://scilib.ai/kg/mathlib#not_isSquare_of_neg

← MathLib Explorer

English

If x < 0, then x is not a square.

Русский

Если x < 0, то x не является квадратом.

LaTeX

$$$x < 0 \Rightarrow \neg \exists y, x = y^2.$$$

Lean4

@[simp]
theorem not_isSquare_of_neg [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] {x : R}
    (h : x < 0) : ¬IsSquare x :=
  (h.not_ge ·.nonneg)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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