toHom_one

Mathlib.LinearAlgebra.RootSystem.Hom

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

English

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

Русский

Обратная кoweight-карта эквивалентности равна обратной кoweight-карте.

LaTeX

$$$ (symm P Q f).coweightMap = (coweightEquiv P Q f)^{-1} $$$

Lean4

@[simp]
theorem toHom_one (P : RootPairing ι R M N) : (1 : RootPairing.Equiv P P).toHom = (1 : RootPairing.Hom P P) :=
  rfl

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

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

Разделы

Аффилиация

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