mem_sumSq

Mathlib.Algebra.Ring.SumsOfSquares

URI: https://scilib.ai/kg/mathlib#NonUnitalSubsemiring.mem_sumSq

English

For NonUnitalSubsemiring T, an element s belongs to sumSq T if and only if IsSumSq s.

Русский

Для NonUnitalSubsemiring T элемент s принадлежит sumSq T тогда и только тогда, когда IsSumSq s.

LaTeX

$$$s \in \mathrm{sumSq}\, T \; \Leftrightarrow\; \operatorname{IsSumSq}(s)$$$

Lean4

@[simp]
theorem mem_sumSq {s : T} : s ∈ sumSq T ↔ IsSumSq s := by simp [← NonUnitalSubsemiring.mem_toAddSubmonoid]

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

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

Разделы

Аффилиация

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