toCoweightBasis_repr_coroot

Mathlib.LinearAlgebra.RootSystem.Base

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

← MathLib Explorer

English

For i, j ∈ b.support with i ≠ j, the difference P.root(i) - P.root(j) is not in the range of P.root.

Русский

Для i, j ∈ b.support, i ≠ j, разность P.root(i) - P.root(j) не лежит в диапазоне P.root.

LaTeX

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

Lean4

@[simp]
theorem toCoweightBasis_repr_coroot (i : b.support) : b.toCoweightBasis.repr (P.coroot i) = Finsupp.single i 1 := by
  simp [← LinearEquiv.eq_symm_apply]

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

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

Разделы

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

Аффилиация

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