exists_bilinForm_self_ne_zero — Mathlib

English

There exists an orthogonal basis for a symmetric bilinear form on a finite-dimensional vector space over a field with invertible 2.

Русский

Существует ортогональный базис для симметричной билинейной формы на конечномерном пространстве над полем, где 2 обратимая.

LaTeX

$$exists_orthogonal_basis$$

Lean4

/-- There exists a non-null vector with respect to any symmetric, nonzero bilinear form `B`
on a module `M` over a ring `R` with invertible `2`, i.e. there exists some
`x : M` such that `B x x ≠ 0`. -/
theorem exists_bilinForm_self_ne_zero [htwo : Invertible (2 : R)] {B : BilinForm R M} (hB₁ : B ≠ 0) (hB₂ : B.IsSymm) :
    ∃ x, ¬B.IsOrtho x x := by
  lift B to QuadraticForm R M using hB₂ with Q
  obtain ⟨x, hx⟩ := QuadraticMap.exists_quadraticMap_ne_zero hB₁
  exact ⟨x, fun h => hx (Q.associated_eq_self_apply ℕ x ▸ h)⟩

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