separatingLeft_of_anisotropic — Mathlib

English

There exists a nonzero x with B(x,x) ≠ 0 for any symmetric, nonzero bilinear form with invertible 2.

Русский

Существует ненулевой вектор x такой, что B(x,x) ≠ 0 для любой симметричной ненулевой билинейной формы при обратимости 2.

LaTeX

$$∃ x, ¬B.IsOrtho x x$$

Lean4

/-- A bilinear form is separating left if the quadratic form it is associated with is anisotropic.
-/
theorem separatingLeft_of_anisotropic {B : BilinForm R M} (hB : B.toQuadraticMap.Anisotropic) : B.SeparatingLeft :=
  fun x hx => hB _ (hx x)

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