not_isSumSq_neg_one

Mathlib.Algebra.Ring.Semireal.Defs

URI: https://scilib.ai/kg/mathlib#IsSemireal.not_isSumSq_neg_one

← MathLib Explorer

English

In a semireal ring, −1 is not a sum of squares.

Русский

В полусуществующем кольце −1 не является суммой квадратов.

LaTeX

$$$\neg IsSumSq(-1)$$$

Lean4

/-- In a semireal ring, `-1` is not a sum of squares. -/
theorem not_isSumSq_neg_one [AddGroup R] [One R] [Mul R] [IsSemireal R] : ¬IsSumSq (-1 : R) :=
  (by simpa using one_add_ne_zero ·)

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

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

Разделы

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

Аффилиация

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