instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem

English

The crystallographic property holds for the root system associated to the Cartan subalgebra of the Lie algebra.

Русский

Кристаллическое свойство сохраняется для корневой системы, связанной с Cartan-подалгеброй алгебры Ли.

LaTeX

$$(rootSystem(H)).IsCrystallographic$$

Lean4

instance : (rootSystem H).IsCrystallographic where
  exists_value α β := ⟨chainBotCoeff β.1 α.1 - chainTopCoeff β.1 α.1, by simp [apply_coroot_eq_cast β.1 α.1]⟩

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