sumsq_nonneg

Mathlib.NumberTheory.Dioph

URI: https://scilib.ai/kg/mathlib#Poly.sumsq_nonneg

← MathLib Explorer

English

Negation commutes with evaluation: for all a, (−f)(a) = −f(a).

Русский

Отрицание при вычислении полиномов сохраняется: (−f)(a) = −f(a).

LaTeX

$$$$ (-f)(a) = -f(a) $$$$

Lean4

theorem sumsq_nonneg (x : α → ℕ) : ∀ l, 0 ≤ sumsq l x
  | [] => le_refl 0
  | p :: ps => by
    rw [sumsq]
    exact add_nonneg (mul_self_nonneg _) (sumsq_nonneg _ ps)

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

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

Разделы

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

Аффилиация

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