sub_notMem_range_coroot

Mathlib.LinearAlgebra.RootSystem.Base

URI: https://scilib.ai/kg/mathlib#RootPairing.Base.sub_notMem_range_coroot

← MathLib Explorer

English

Same statement as above for coroots: P.coroot(i) - P.coroot(j) ∉ range P.coroot.

Русский

То же самое для короот: P.coroot(i) - P.coroot(j) ∉ range P.coroot.

LaTeX

$$P.coroot i - P.coroot j ∉ range P.coroot$$

Lean4

theorem sub_notMem_range_coroot {i j : ι} (hi : i ∈ b.support) (hj : j ∈ b.support) :
    P.coroot i - P.coroot j ∉ range P.coroot :=
  b.flip.sub_notMem_range_root hi hj

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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