isOrtho_def

Mathlib.LinearAlgebra.QuadraticForm.Basic

URI: https://scilib.ai/kg/mathlib#QuadraticMap.isOrtho_def

English

IsOrtho Q x y is equivalent to Q(x+y) = Q(x) + Q(y).

Русский

IsOrtho Q x y эквивалентно Q(x+y) = Q(x) + Q(y).

LaTeX

$$$\\text{IsOrtho}(Q,x,y) \\iff Q(x+y)=Q(x)+Q(y).$$$

Lean4

theorem isOrtho_def {Q : QuadraticMap R M N} {x y : M} : Q.IsOrtho x y ↔ Q (x + y) = Q x + Q y :=
  Iff.rfl

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

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

Разделы

Аффилиация

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