weightMap_one

Mathlib.LinearAlgebra.RootSystem.Hom

URI: https://scilib.ai/kg/mathlib#RootPairing.Hom.weightMap_one

English

The weight map of the identity morphism is the identity map on weight spaces.

Русский

Весовое отображение тождества равно тождественному отображению на весовых пространствах.

LaTeX

$$weightMap (P:=P) (Q:=P) 1 = id$$

Lean4

@[simp]
theorem weightMap_one (P : RootPairing ι R M N) : weightMap (P := P) (Q := P) 1 = LinearMap.id (R := R) (M := M) :=
  rfl

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

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

Разделы

Аффилиация

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