exists_quadraticMap_ne_zero — Mathlib

English

If the associated bilinear form of a quadratic map Q is nonzero, then there exists a vector x with Q(x) ≠ 0.

Русский

Если связанная билинейная форма квадратичной карты Q не нулевая, существует вектор x такой, что Q(x) ≠ 0.

LaTeX

$$$\\forall Q:\\mathrm{QuadraticMap}(R,M,N),\\; (\\mathrm{associated'}(Q)\\neq 0)\\Rightarrow \\exists x:\\!M,\\; Q(x)\\neq 0.$$$

Lean4

/-- There exists a non-null vector with respect to any quadratic form `Q` whose associated
bilinear form is non-zero, i.e. there exists `x` such that `Q x ≠ 0`. -/
theorem exists_quadraticMap_ne_zero
    {Q : QuadraticMap R M N}
      -- Porting note: added implicit argument

    (hB₁ : associated' (N := N) Q ≠ 0) : ∃ x, Q x ≠ 0 :=
  by
  rw [← not_forall]
  intro h
  apply hB₁
  rw [(QuadraticMap.ext h : Q = 0), LinearMap.map_zero]

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