isSymm_posForm

Mathlib.LinearAlgebra.RootSystem.RootPositive

URI: https://scilib.ai/kg/mathlib#RootPairing.RootPositiveForm.isSymm_posForm

English

There is a relation that connects rootLength with posForm and form via equality lemmas (eq_1).

Русский

Существует связь между rootLength, posForm и form через равенства (eq_1).

LaTeX

$$$ B.rootLength i = \\text{(expression from eq_1)} $$$

Lean4

theorem isSymm_posForm : B.posForm.IsSymm where
  eq x
    y := by
    apply FaithfulSMul.algebraMap_injective S R
    simpa using B.symm.eq x y

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru