span_coroot'_eq_top

Mathlib.LinearAlgebra.RootSystem.IsValuedIn

URI: https://scilib.ai/kg/mathlib#RootPairing.span_coroot'_eq_top

English

If B is symmetric, the reflection across the coroot is orthogonal with respect to B.

Русский

Если B симметрична, отражение через корoot ортогонально относительно B.

LaTeX

$$B.IsSymm → B.IsOrthogonal (Module.reflection (coroot_apply_self B hx))$$

Lean4

@[simp]
theorem span_coroot'_eq_top (P : RootSystem ι R M N) : span R (range P.coroot') = ⊤ :=
  span_root'_eq_top P.flip

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

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

Разделы

Аффилиация

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