posRootForm — Mathlib

English

The algebra map sends posRootForm.posForm to RootForm.

Русский

Алгебраическое отображение переводит posRootForm.posForm в RootForm.

LaTeX

$$$\\mathrm{algebraMap}\ S R\\bigl((P.posRootForm S).posForm\\bigr) = P.RootForm$$

Lean4

/-- The bilinear form of a finite root pairing taking values in a linearly-ordered ring, as a
root-positive form. -/
def posRootForm : P.RootPositiveForm S where
  form := P.RootForm
  symm := P.rootForm_symmetric
  isOrthogonal_reflection := P.rootForm_reflection_reflection_apply
  exists_eq i j := ⟨∑ k, P.pairingIn S i k * P.pairingIn S j k, by simp [rootForm_apply_apply]⟩
  exists_pos_eq
    i := by
    refine ⟨∑ k, P.pairingIn S i k ^ 2, ?_, by simp [sq, rootForm_apply_apply]⟩
    exact Finset.sum_pos' (fun j _ ↦ sq_nonneg _) ⟨i, by simp⟩

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