weightEquiv_inv

Mathlib.LinearAlgebra.RootSystem.Hom

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

← MathLib Explorer

English

WeightEquiv respects inverses: weightEquiv P P g^{-1} equals (weightEquiv P P g)^{-1}.

Русский

WeightEquiv сохраняет обратное: weightEquiv P P g^{-1} = (weightEquiv P P g)^{-1}.

LaTeX

$$$ weightEquiv P P g^{-1} = (weightEquiv P P g)^{-1}. $$$

Lean4

@[simp]
theorem weightEquiv_inv {P : RootPairing ι R M N} (g : Aut P) : weightEquiv P P g⁻¹ = (weightEquiv P P g)⁻¹ :=
  LinearEquiv.toLinearMap_inj.mp rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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