rootForm_nondegenerate — Mathlib

English

If P is an anisotropic RootSystem, then the RootForm is a nondegenerate bilinear form.

Русский

Если P является анизотропной корневой системой, то корневая форма является невырожденной билинейной формой.

LaTeX

$$$\\forall x \\in P.rootSpan R\\,\\, (\\forall y \\in P.rootSpan R,\\ P.RootForm x y = 0) \\Rightarrow x = 0$$$

Lean4

theorem _root_.RootSystem.rootForm_nondegenerate (P : RootSystem ι R M N) [P.IsAnisotropic] :
    P.RootForm.Nondegenerate :=
  LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot.mpr <| by simpa using P.disjoint_rootSpan_ker_rootForm

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