orthogonal_corootSpan_eq

Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

URI: https://scilib.ai/kg/mathlib#RootPairing.orthogonal_corootSpan_eq

English

The orthogonal of the coroot span with respect to CorootForm equals the kernel of CorootForm.

Русский

Ортогональное дополнение к corootSpan относительно CorootForm равно ker CorootForm.

LaTeX

$$P.CorootForm.orthogonal (P.corootSpan R) = LinearMap.ker P.CorootForm$$

Lean4

@[simp]
theorem orthogonal_corootSpan_eq : P.CorootForm.orthogonal (P.corootSpan R) = LinearMap.ker P.CorootForm :=
  P.flip.orthogonal_rootSpan_eq

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

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

Разделы

Аффилиация

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