coweightEquiv_one

Mathlib.LinearAlgebra.RootSystem.Hom

URI: https://scilib.ai/kg/mathlib#RootPairing.Equiv.coweightEquiv_one

English

The weight map of the inverse equivalence equals the inverse of the weight map.

Русский

Весовая карта обратного эквивалентности равна обратной весовой карте.

LaTeX

$$$ (symm P Q f).weightMap = (weightEquiv P Q f)^{-1} $$$

Lean4

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

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

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

Разделы

Аффилиация

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