orthogonal_span_singleton_eq_toLin_ker

English

For a bilinear form B and vector x, the orthogonal to the span of x equals the kernel of the linear map y ↦ B(x,y).

Русский

Для билинейной формы B и вектора x ортогональность к спану x равна ядру линейного отображения y ↦ B(x,y).

LaTeX

$$$B.orthogonal(K \cdot x) = \ker( y \mapsto B(x,y) )$$$

Lean4

theorem orthogonal_span_singleton_eq_toLin_ker {B : BilinForm K V} (x : V) :
    B.orthogonal (K ∙ x) = LinearMap.ker (LinearMap.BilinForm.toLinHomAux₁ B x) :=
  by
  ext y
  simp_rw [mem_orthogonal_iff, LinearMap.mem_ker, Submodule.mem_span_singleton]
  constructor
  · exact fun h => h x ⟨1, one_smul _ _⟩
  · rintro h _ ⟨z, rfl⟩
    rw [IsOrtho, smul_left, mul_eq_zero]
    exact Or.intro_right _ h

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