English
An orthogonal basis w.r.t. a bilinear form B yields nondegeneracy if and only if no basis vector is self-orthogonal.
Русский
Ортогональная база по билинейной форме B даёт недегнерируемость тогда и только тогда, когда ни один вектор базы не сам-ортогонален.
LaTeX
$$B.iIsOrtho v → (B.Nondegenerate ↔ ∀ i, ¬ B.IsOrtho (v i) (v i))$$
Lean4
/-- Given an orthogonal basis with respect to a bilinear form, the bilinear form is nondegenerate
iff the basis has no elements which are self-orthogonal. -/
theorem nondegenerate_iff_not_isOrtho_basis_self {n : Type w} [Nontrivial R] [NoZeroDivisors R] (B : BilinForm R M)
(v : Basis n R M) (hO : B.iIsOrtho v) : B.Nondegenerate ↔ ∀ i, ¬B.IsOrtho (v i) (v i) :=
by
refine ⟨hO.not_isOrtho_basis_self_of_nondegenerate, fun ho m hB => ?_⟩
obtain ⟨vi, rfl⟩ := v.repr.symm.surjective m
rw [LinearEquiv.map_eq_zero_iff]
ext i
rw [Finsupp.zero_apply]
specialize hB (v i)
simp_rw [Basis.repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum, sum_left, smul_left] at hB
rw [Finset.sum_eq_single i] at hB
· exact eq_zero_of_ne_zero_of_mul_right_eq_zero (ho i) hB
· intro j _ hij
convert mul_zero (vi j) using 2
exact hO hij
· intro hi
convert zero_mul (M₀ := R) _ using 2
exact Finsupp.notMem_support_iff.mp hi
