rootForm_restrict_nondegenerate_of_ordered

English

The kernel of RootForm equals the image of the dual annihilator of rootSpan under the perfect pairing map.

Русский

Ядро RootForm совпадает с образов двойного аннигилирующего подпространства корневого Span через попаривание.

LaTeX

$$P.ker_rootForm_eq_dualAnnihilator$$

Lean4

/-- See also `RootPairing.rootForm_restrict_nondegenerate_of_isAnisotropic`. -/
theorem rootForm_restrict_nondegenerate_of_ordered : LinearMap.Nondegenerate (P.RootForm.restrict (P.rootSpan R)) :=
  (P.RootForm.nondegenerate_restrict_iff_disjoint_ker P.zero_le_rootForm P.rootForm_symmetric).mpr
    P.disjoint_rootSpan_ker_rootForm

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