not_isOrtho_basis_self_of_nondegenerate

English

An orthogonal basis with respect to a nondegenerate bilinear form has no self-orthogonal elements.

Русский

Ортогональная база по отношению к неdegenerate билинейной форме не содержит элементов, ортогональных самим себе.

LaTeX

$$Not (B.IsOrtho v v) → IsCompl(span{v_i}, B.orthogonal(span{v_i}))$$

Lean4

/-- An orthogonal basis with respect to a nondegenerate bilinear form has no self-orthogonal
elements. -/
theorem not_isOrtho_basis_self_of_nondegenerate {n : Type w} [Nontrivial R] {B : BilinForm R M} {v : Basis n R M}
    (h : B.iIsOrtho v) (hB : B.Nondegenerate) (i : n) : ¬B.IsOrtho (v i) (v i) :=
  by
  intro ho
  refine v.ne_zero i (hB (v i) fun m => ?_)
  obtain ⟨vi, rfl⟩ := v.repr.symm.surjective m
  rw [Basis.repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum, sum_right]
  apply Finset.sum_eq_zero
  rintro j -
  rw [smul_right]
  convert mul_zero (vi j) using 2
  obtain rfl | hij := eq_or_ne i j
  · exact ho
  · exact h hij

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