separatingRight_iff_not_isOrtho_basis_self

English

If an orthogonal basis has no self-orthogonal vectors, then the bilinear form is right-separating.

Русский

Если базис не имеет self-orthogonal элементов, форма правосторонне разделяет.

LaTeX

$$B.SeparatingRight$$

Lean4

/-- Given an orthogonal basis with respect to a bilinear map, the bilinear map is right-separating
if the basis has no elements which are self-orthogonal. -/
theorem separatingRight_iff_not_isOrtho_basis_self [NoZeroSMulDivisors R M₁] {B : M →ₗ[R] M →ₗ[R] M₁} (v : Basis n R M)
    (hO : B.IsOrthoᵢ v) (h : ∀ i, ¬B.IsOrtho (v i) (v i)) : B.SeparatingRight :=
  by
  rw [isOrthoᵢ_flip] at hO
  rw [← flip_separatingLeft]
  refine IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self v hO fun i ↦ ?_
  rw [isOrtho_flip]
  exact h i

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