ne_zero_of_not_isOrtho_self

Mathlib.LinearAlgebra.QuadraticForm.Basic

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

English

If Q.IsOrtho x x is false, then x ≠ 0.

Русский

Если Q.IsOrtho x x ложно, то x ≠ 0.

LaTeX

$$$\\forall x:\\; \\neg Q.IsOrtho\\,x\\,x \\Rightarrow x \\neq 0.$$$

Lean4

theorem ne_zero_of_not_isOrtho_self {Q : QuadraticMap R M N} (x : M) (hx₁ : ¬Q.IsOrtho x x) : x ≠ 0 := fun hx₂ =>
  hx₁ (hx₂.symm ▸ .zero_left _)

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

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

Разделы

Аффилиация

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