coweightMap_one

Mathlib.LinearAlgebra.RootSystem.Hom

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

English

The coweight map of the identity morphism is the identity on the dual weight space.

Русский

Противовесное отображение тождества на двойственном весовом пространстве является тождественным.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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