Anisotropic

Mathlib.LinearAlgebra.QuadraticForm.Basic

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

English

If Q.IsOrtho x y, then the polar bilinear form polar Q x y equals 0.

Русский

Если QIsOrtho x y, то полярная билинейная форма polar Q x y равна нулю.

LaTeX

$$$\\mathrm{polar}(Q,x,y)=0 \\quad\\text{iff}\\quad \\mathrm{IsOrtho}(Q,x,y).$$$

Lean4

/-- An anisotropic quadratic map is zero only on zero vectors. -/
def Anisotropic (Q : QuadraticMap R M N) : Prop :=
  ∀ x, Q x = 0 → x = 0

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

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

Разделы

Аффилиация

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