not_linearIndependent_of_apply_mul_apply_eq

English

Nondegenerate bilinear form is equivalent to a strong form of separating properties.

Русский

Невырожденная билинейная форма эквивалентна сильной форме разделения.

LaTeX

$$nondegenerate_iff_separatingLeft$$

Lean4

/-- The equality case of **Cauchy-Schwarz**. -/
theorem not_linearIndependent_of_apply_mul_apply_eq (hp : ∀ x, x ≠ 0 → 0 < B x x) (x y : M)
    (he : (B x y) * (B y x) = (B x x) * (B y y)) : ¬LinearIndependent R ![x, y] :=
  by
  have hz : (B x y) • x - (B x x) • y = 0 := by
    by_contra hc
    exact
      (ne_of_lt (hp ((B x) y • x - (B x) x • y) hc)).symm <|
        (apply_smul_sub_smul_sub_eq B x y).symm ▸ (mul_eq_zero_of_right ((B x) x) (sub_eq_zero_of_eq he.symm))
  by_contra hL
  by_cases hx : x = 0
  · simpa [hx] using LinearIndependent.ne_zero 0 hL
  · have h := sub_eq_zero.mpr (sub_eq_zero.mp hz).symm
    rw [sub_eq_add_neg, ← neg_smul, add_comm] at h
    exact (Ne.symm (ne_of_lt (hp x hx))) (LinearIndependent.eq_zero_of_pair hL h).2

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