posRootForm_posForm_nondegenerate

English

Disjointness of rootSpan and ker RootForm is established, i.e., their intersection is {0}.

Русский

Установлена дизъюнктность корневого пространства и ядра RootForm; пересечение — ноль.

LaTeX

$$Disjoint (P.rootSpan R) (LinearMap.ker P.RootForm)$$

Lean4

theorem posRootForm_posForm_nondegenerate : (P.posRootForm S).posForm.Nondegenerate :=
  by
  refine LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot.mpr <| LinearMap.ker_eq_bot'.mpr ?_
  intro x hx
  contrapose! hx
  rw [DFunLike.ne_iff]
  use x
  exact (posRootForm_posForm_pos_of_ne_zero P S hx).ne'

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