zero_le_rootForm

Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

URI: https://scilib.ai/kg/mathlib#RootPairing.zero_le_rootForm

English

For any x, the value of RootForm on (x,x) is nonnegative.

Русский

Для любого x значение RootForm на (x,x) неотрицательно.

LaTeX

$$0 \\le P.RootForm x x$$

Lean4

theorem zero_le_rootForm (x : M) : 0 ≤ P.RootForm x x :=
  (P.rootForm_self_sum_of_squares x).nonneg

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

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

Разделы

Аффилиация

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