separatingLeft_of_anisotropic — Mathlib

English

An anisotropic quadratic map has a nondegenerate associated bilinear form; specifically, it is separating on the left.

Русский

У анизотропной квадратичной формы связанная билинейная форма ненулевой левой сепарации; она неизоморфна слева.

LaTeX

$$$\\text{If } Q\\text{ is anisotropic and } 2\\text{ is invertible, then } (\\mathrm{associated}'(Q)).\\mathrm{SeparatingLeft}.$$$

Lean4

/-- The associated bilinear form of an anisotropic quadratic form is nondegenerate. -/
theorem separatingLeft_of_anisotropic [Invertible (2 : R)] (Q : QuadraticMap R M R) (hB : Q.Anisotropic) :
    -- Porting note: added implicit argument
    (QuadraticMap.associated' (N := R) Q).SeparatingLeft := fun x hx ↦
  hB _ <| by
    rw [← hx x]
    exact (associated_eq_self_apply _ _ x).symm

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