mem_of_isSumSq

Mathlib.Algebra.Order.Ring.Ordering.Basic

URI: https://scilib.ai/kg/mathlib#RingPreordering.mem_of_isSumSq

← MathLib Explorer

English

If x is a sum of squares in a RingPreordering, then x ∈ P.

Русский

Если x представимо как сумма квадратов, то x ∈ P.

LaTeX

$$If $x$ is a sum of squares, then $x ∈ P$$$

Lean4

@[aesop unsafe 80% apply (rule_sets := [SetLike])]
theorem mem_of_isSumSq {x : R} (hx : IsSumSq x) : x ∈ P := by induction hx using IsSumSq.rec' <;> aesop

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

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

Разделы

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

Аффилиация

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